aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2003-11-12 04:32:00 +0000
committerletouzey2003-11-12 04:32:00 +0000
commit06807ca5dab501303aa63571838813ab388d7097 (patch)
treeac285d10ed6c531548c0dfb6651eeb6b88185108
parent2698a4a1786527ef9edb4848077d62e655c1481e (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8352 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/.cvsignore4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore
index 0f2afaa291..90d61db14d 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -3,8 +3,8 @@
*.ilg
*.v.tex
*.pdf
-euclid.ml
-heapsort.ml
+euclid.ml*
+heapsort.ml*
avl.ml
*.bbl
www