From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 6 Feb 2004 12:25:11 +0000 (+0000)
Subject: ignore .debug_script (used by Makefile's debug target)
X-Git-Tag: V_0_2_3~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de9aae3754cc79baadb00d62a6433579d621e301;p=helm.git

ignore .debug_script (used by Makefile's debug target)
---

diff --git a/helm/gTopLevel/.cvsignore b/helm/gTopLevel/.cvsignore
index ea4665c4b..09c78cec5 100644
--- a/helm/gTopLevel/.cvsignore
+++ b/helm/gTopLevel/.cvsignore
@@ -6,3 +6,4 @@ styles stylesheets meta_stylesheets
 chosenTermEditor.ml
 chosenTransformer.ml
 disambiguatingParser.ml
+.debug_script