From: Claudio Sacerdoti Coen Date: Thu, 30 Nov 2000 15:50:08 +0000 (+0000) Subject: ominidom.cmi not installed by Makefile X-Git-Tag: nogzip~128 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=48251720121a3eeaa444a5488e2f7b0db82cb380;p=helm.git ominidom.cmi not installed by Makefile --- diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/minidom/Makefile b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/minidom/Makefile index 15f84731a..9b50d8333 100644 --- a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/minidom/Makefile +++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/minidom/Makefile @@ -1,6 +1,6 @@ LIBDIR = /usr/lib/ocaml INSTALLDIR = $(LIBDIR)/minidom -OBJECTS = minidom.cmi minidom.cmo ml_minidom.o ominidom.cmo +OBJECTS = minidom.cmi minidom.cmo ml_minidom.o ominidom.cmi ominidom.cmo OBJECTS_OPT = minidom.cmx ominidom.cmx INST = minidom.o ominidom.o ml_minidom.h minidom.mli