diff options
Diffstat (limited to 'etc/headache_config')
| -rw-r--r-- | etc/headache_config | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/etc/headache_config b/etc/headache_config index 23bed5e..203f888 100644 --- a/etc/headache_config +++ b/etc/headache_config @@ -4,4 +4,3 @@ | ".*\\.thy" -> frame open:"(*" line:"=" close:"*)" | ".*\\.sml" -> frame open:"(*" line:"=" close:"*)" | ".*\\.sail" -> frame open:"/*" line:"=" close:"*/" - |