summaryrefslogtreecommitdiff
path: root/etc/headache_config
diff options
context:
space:
mode:
authorRobert Norton2018-07-10 12:20:01 +0100
committerRobert Norton2018-07-10 12:20:09 +0100
commitca40c5ae8f89aa3268bdc69125107c62c9240a4c (patch)
treec1f5b847b853ae0b304ab30486d2736895960280 /etc/headache_config
parent58836205da846571afdb7994a9d5915f6fbae09f (diff)
further anonymisation work.
Diffstat (limited to 'etc/headache_config')
-rw-r--r--etc/headache_config2
1 files changed, 2 insertions, 0 deletions
diff --git a/etc/headache_config b/etc/headache_config
index 4a68f1ef..23bed5ea 100644
--- a/etc/headache_config
+++ b/etc/headache_config
@@ -1,5 +1,7 @@
".*\\.mllib" -> frame open:"(*" line:"=" close:"*)"
| ".*\\.lem" -> frame open:"(*" line:"=" close:"*)"
| ".*\\.v" -> frame open:"(*" line:"=" close:"*)"
+| ".*\\.thy" -> frame open:"(*" line:"=" close:"*)"
+| ".*\\.sml" -> frame open:"(*" line:"=" close:"*)"
| ".*\\.sail" -> frame open:"/*" line:"=" close:"*/"