summaryrefslogtreecommitdiff
path: root/common
diff options
context:
space:
mode:
authorstuebinm2026-01-18 15:13:37 +0100
committerstuebinm2026-01-18 15:13:37 +0100
commit9eb9292be4468b5b36fe4217b4f92f8a92c668f6 (patch)
tree0fa4d8f2c9265fc35e8357262c41b4bbf0f6dfaa /common
parent0d709caed396d24acea583971d4e3c4e5b7c5673 (diff)
home: make git produce useful diffs on .thy filesHEADmain
Diffstat (limited to 'common')
0 files changed, 0 insertions, 0 deletions