]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/.cvsignore
ignore .debug_script (used by Makefile's debug target)
[helm.git] / helm / gTopLevel / .cvsignore
index ea4665c4ba04ade2dd89bd6b731951bbb395a71f..09c78cec59b72904f73766196f89480331e23e71 100644 (file)
@@ -6,3 +6,4 @@ styles stylesheets meta_stylesheets
 chosenTermEditor.ml
 chosenTransformer.ml
 disambiguatingParser.ml
+.debug_script