summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2015-04-24 10:01:56 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2015-04-24 10:01:56 -0400
commite397773585d073cfb089e7a2f2b038ea3c60a4a4 (patch)
tree4c45ceb81a24d87ef7fa83669dababa10b16b36f
parent8f422a4f4b96211b5319ba0f3023948f53d5ff10 (diff)
Ignore manual.out
-rw-r--r--.hgignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.hgignore b/.hgignore
index c3272f05..20e290b8 100644
--- a/.hgignore
+++ b/.hgignore
@@ -34,6 +34,7 @@ demo/more/out/*.html
demo/more/demo.*
doc/*.html
+doc/*.out
*.sql
*mlmon.out