]> 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: 133ffec)
Unused variable removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 13 Nov 2001 18:06:38 +0000 (18:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 13 Nov 2001 18:06:38 +0000 (18:06 +0000)
helm/DEVEL/mlminidom/Makefile.in patch | blob | history

diff --git a/helm/DEVEL/mlminidom/Makefile.in b/helm/DEVEL/mlminidom/Makefile.in
index e82872538f71dc7ef9144df1c1d737a1cdbe7046..ecd1c83869c85b2be86ed9aea5ddff5ea04b25b0 100644 (file)
--- a/helm/DEVEL/mlminidom/Makefile.in
+++ b/helm/DEVEL/mlminidom/Makefile.in
@@ -3,7 +3,6 @@ VERSION = @VERSION@
 INCLUDEDIR = @OCAML_INCLUDE_DIR@
 LIBDIR = @OCAML_LIB_DIR@
 PREFIX = 
-INSTALLDIR = $(PREFIX)$(LIBDIR)/$(PACKAGE)
 OBJECTS_C = ml_minidom.o
 OBJECTS = minidom.cmo ominidom.cmo
 OBJECTS_OPT = minidom.cmx ominidom.cmx
Unnamed repository; edit this file 'description' to name the repository.