summaryrefslogtreecommitdiff
path: root/.hgignore
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-30 17:15:14 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-30 17:15:14 -0400
commit2570fc6449706fd93641ab23762194dbcd50db09 (patch)
tree4be9b76a5e655b9f28be47710cc47e600a369a14 /.hgignore
parent82825a3ba67f3a01d8a3658c74d8171dcd21276e (diff)
C FFI compiler options
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