From: Ferruccio Guidi Date: Fri, 6 Aug 2010 23:26:57 +0000 (+0000) Subject: ld.dtd: updated to comply with crg X-Git-Tag: make_still_working~2844 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f57c2060459d2b55567447b70590bc5a26933cc7;p=helm.git ld.dtd: updated to comply with crg Makefiles: updated to comply with new HELM server configuration top: some traces of old command line option "-m" removed --- diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index a6fcf6c48..353b70187 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -15,7 +15,11 @@ TAGS = test-si test-si-fast hal xml-si-crg xml-si profile XMLS = xml/brg-si/grundlagen/l/not.ld.xml \ xml/brg-si/grundlagen/l/et.ld.xml \ xml/brg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ - xml/brg-si/grundlagen/l/e/pairis1.ld.xml + xml/brg-si/grundlagen/l/e/pairis1.ld.xml \ + xml/crg-si/grundlagen/l/not.ld.xml \ + xml/crg-si/grundlagen/l/et.ld.xml \ + xml/crg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ + xml/crg-si/grundlagen/l/e/pairis1.ld.xml include Makefile.common @@ -37,10 +41,6 @@ profile: $(MAIN).opt etc $(H)for T in `seq 30`; do ./$(MAIN).opt -u -q -s 3 -S 1 $(O) $(INPUT) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt -hal: $(MAIN).opt etc - @echo " HELENA -o -x -m $(INPUT)" - $(H)./$(MAIN).opt -o -x $(HOME) -m -s 1 -S 1 $(INPUT) > etc/log.txt - xml-si: $(MAIN).opt etc @echo " HELENA -u -x -s 2 $(INPUT)" $(H)./$(MAIN).opt -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt @@ -76,9 +76,13 @@ lddl: index @echo " GENERATE lddl.tar.bz2" $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X etc/exclude.txt xml +install-dtd: xml/ld.dtd + @echo " INSTALL $<" + $(H)scp $< $(XMLDIR) + install-xml: etc/make-html.sh @echo " INSTALL xml" - cp -a xml/index.txt xml/ld.dtd xml/brg-si/ $(XMLDIR) + $(H)cp -a xml/index.txt xml/ld.dtd xml/brg-si/ $(XMLDIR) # old targets ########################################################## diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index e3b12db51..7ab5447b6 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -6,9 +6,9 @@ else endif LDDLURL = http://helm.cs.unibo.it/lambda-delta/static/lddl -LDDLDIR = /projects/helm/public_html/lambda-delta/static/lddl -DOWNDIR = /projects/helm/public_html/lambda-delta/download -XMLDIR = /projects/helm/public_html/lambda-delta/xml +LDDLDIR = mowgli:/projects/helm/public_html/lambda-delta/static/lddl +DOWNDIR = mowgli:/projects/helm/public_html/lambda-delta/download +XMLDIR = mowgli:/projects/helm/public_html/lambda-delta/xml DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make)) diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index be3059ea2..40a58673a 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -327,7 +327,7 @@ try flush_all () in let help = - "Usage: helena [ -LPVXcgijmopqu1 | -Ss | -x | -hkr ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXcgijopqu1 | -Ss | -x | -hkr ]* [ ]*\n\n" ^ "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd index 1a3103c2a..e6e90f738 100644 --- a/helm/software/lambda-delta/xml/ld.dtd +++ b/helm/software/lambda-delta/xml/ld.dtd @@ -10,6 +10,8 @@ + + - + - + - +