diff options
| -rw-r--r-- | doc/.cvsignore | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore index 0f2afaa29..90d61db14 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 |