]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 4d9a43f)
patched for *.cmx
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 12 Feb 2004 22:07:05 +0000 (22:07 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 12 Feb 2004 22:07:05 +0000 (22:07 +0000)
helm/ocaml/registry/.cvsignore patch | blob | history

diff --git a/helm/ocaml/registry/.cvsignore b/helm/ocaml/registry/.cvsignore
index fbe20a217eb1f2e58f22eeae7b08af504225a3ca..702419146101e74327791c5a7203b787e7525137 100644 (file)
--- a/helm/ocaml/registry/.cvsignore
+++ b/helm/ocaml/registry/.cvsignore
@@ -4,3 +4,4 @@
 *.cmo
 *.cmxa
 *.o
+*.cmx
Unnamed repository; edit this file 'description' to name the repository.