From fb8ca50af3bb9392b66505b28ba718c90f8ab0ab Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Fri, 3 Feb 2017 14:54:22 +0000
Subject: fix headers

---
 etc/headache_config | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'etc')

diff --git a/etc/headache_config b/etc/headache_config
index a9d518f1..e8745fee 100644
--- a/etc/headache_config
+++ b/etc/headache_config
@@ -1,2 +1,3 @@
-  ".*\\.lem"    -> frame open:"(*" line:"=" close:"*)"
-| ".*\\.sail"   -> frame open:"(*" line:"=" close:"*)"
+  ".*\\.mllib"  -> frame open:"(*" line:"=" close:"*)"
+|  ".*\\.lem"    -> frame open:"(*" line:"=" close:"*)"
+|  ".*\\.sail"   -> frame open:"(*" line:"=" close:"*)"
-- 
cgit v1.2.3