]> 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: 9a0385e)
...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 27 Nov 2008 21:29:23 +0000 (21:29 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 27 Nov 2008 21:29:23 +0000 (21:29 +0000)
helm/software/components/ng_disambiguation/.depend.opt patch | blob | history

diff --git a/helm/software/components/ng_disambiguation/.depend.opt b/helm/software/components/ng_disambiguation/.depend.opt
index 8332733196cfe7e831779b7c44ba86975afc5465..6b4ef95c1ee75472df6140057f1b06851033b996 100644 (file)
--- a/helm/software/components/ng_disambiguation/.depend.opt
+++ b/helm/software/components/ng_disambiguation/.depend.opt
@@ -1,4 +1,2 @@
-nDisambiguate.cmo: nDisambiguate.cmi 
-nDisambiguate.cmx: nDisambiguate.cmi 
-nGrafiteDisambiguator.cmo: nDisambiguate.cmi nGrafiteDisambiguator.cmi 
-nGrafiteDisambiguator.cmx: nDisambiguate.cmx nGrafiteDisambiguator.cmi 
+nCicDisambiguate.cmo: nCicDisambiguate.cmi 
+nCicDisambiguate.cmx: nCicDisambiguate.cmi 
Unnamed repository; edit this file 'description' to name the repository.