]> matita.cs.unibo.it Git - helm.git/commitdiff
removed from repository spurious object files
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 5 Dec 2005 09:22:45 +0000 (09:22 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 5 Dec 2005 09:22:45 +0000 (09:22 +0000)
helm/ocaml/grafite_parser/matitaDisambiguator.cmi [deleted file]
helm/ocaml/grafite_parser/matitaDisambiguator.cmo [deleted file]
helm/ocaml/grafite_parser/matitaDisambiguator.o [deleted file]

diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.cmi b/helm/ocaml/grafite_parser/matitaDisambiguator.cmi
deleted file mode 100644 (file)
index a50009c..0000000
Binary files a/helm/ocaml/grafite_parser/matitaDisambiguator.cmi and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.cmo b/helm/ocaml/grafite_parser/matitaDisambiguator.cmo
deleted file mode 100644 (file)
index fbc548d..0000000
Binary files a/helm/ocaml/grafite_parser/matitaDisambiguator.cmo and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.o b/helm/ocaml/grafite_parser/matitaDisambiguator.o
deleted file mode 100644 (file)
index 5358ead..0000000
Binary files a/helm/ocaml/grafite_parser/matitaDisambiguator.o and /dev/null differ