[r2003-05-26 22:15:09 by cvscast] get rid of Cduce_config

Original author: cvscast
Date: 2003-05-26 22:15:09+00:00

Makefile.distrib

@@ -78,13 +78,6 @@ DTD2CDUCE = tools/dtd2cduce.cmo
 DEPEND = $(DIRS:=/*.ml) $(DIRS:=/*.mli)
 INCLUDES = $(DIRS:%=-I %)
 
-#misc/cduce_config.ml:
-#	sed -e 's|%%VERSION%%|$(VERSION)|' \
-#           -e 's|%%BUILD_DATE%%|$(shell date +%Y-%m-%d)|' \
-#            -e 's|%%NATIVE%%|$(NATIVE)|' \
-#            misc/cduce_config.mlp > misc/cduce_config.ml
-
-
 cduce: $(CDUCE:.cmo=.$(EXTENSION))
 	$(LINK) $(INCLUDES) -o $@ $^