aboutsummaryrefslogtreecommitdiffhomepage
path: root/.hgignore
diff options
context:
space:
mode:
Diffstat (limited to '.hgignore')
-rw-r--r--.hgignore6
1 files changed, 5 insertions, 1 deletions
diff --git a/.hgignore b/.hgignore
index c0222189..f51f3c32 100644
--- a/.hgignore
+++ b/.hgignore
@@ -13,7 +13,6 @@ src/urweb.mlb
*.grm.*
*.o
-./Makefile
src/config.sml
*.exe
@@ -37,3 +36,8 @@ demo/demo.*
.depend
Makefile.coq
*.vo
+
+syntax: regexp
+
+^Makefile
+^src/coq/Makefile