From 782253ebe87375f52c07899c1501db5a665a457f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 10:35:13 +0000 Subject: [PATCH] moved dot stuff to STATS/ --- helm/ocaml/Makefile.in | 22 ++++++++++++++++++---- helm/ocaml/{ => STATS}/clusters.dot | 0 helm/ocaml/{ => STATS}/daemons.dot | 0 helm/ocaml/{ => STATS}/deps.patch | 0 helm/ocaml/{ => STATS}/patch_deps.sh | 6 +++--- 5 files changed, 21 insertions(+), 7 deletions(-) rename helm/ocaml/{ => STATS}/clusters.dot (100%) rename helm/ocaml/{ => STATS}/daemons.dot (100%) rename helm/ocaml/{ => STATS}/deps.patch (100%) rename helm/ocaml/{ => STATS}/patch_deps.sh (90%) diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 337dd0ca0..7ab72ed24 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,3 +1,6 @@ + +export SHELL=/bin/bash + # Warning: the modules must be in compilation order NULL = MODULES = \ @@ -27,7 +30,7 @@ MODULES = \ lexicon \ grafite_engine \ grafite_parser \ - tactics/paramodulation \ + tactics/paramodulation \ $(NULL) OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ @@ -49,10 +52,21 @@ clean: $(MODULES:%=%.clean) clean_metas (for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \ | sort -t : -k 2 -n -r > .stats +EXTRA_DIST_CLEAN = \ + libraries-clusters.ps \ + libraries-clusters.pdf \ + libraries-ext.ps \ + libraries.ps \ + .dep.dot \ + .extdep.dot \ + .clustersdep.dot \ + $(NULL) + clean_metas: rm -f $(METAS) distclean: clean clean_metas - rm -f Makefile Makefile.common configure config.log config.cache config.status + rm -f configure config.log config.cache config.status + rm -f Makefile Makefile.common $(EXTRA_DIST_CLEAN) .PHONY: all opt world metas depend install uninstall clean clean_metas distclean @@ -96,9 +110,9 @@ METAS/META.helm-%: METAS/meta.helm-%.src echo "}" >> $@ .extdep.dot: .dep.dot - ./patch_deps.sh $< $@ + STATS/patch_deps.sh $< $@ .clustersdep.dot: .dep.dot - USE_CLUSTERS=yes ./patch_deps.sh $< $@ + USE_CLUSTERS=yes STATS/patch_deps.sh $< $@ libraries.ps: .dep.dot dot -Tps -o $@ $< diff --git a/helm/ocaml/clusters.dot b/helm/ocaml/STATS/clusters.dot similarity index 100% rename from helm/ocaml/clusters.dot rename to helm/ocaml/STATS/clusters.dot diff --git a/helm/ocaml/daemons.dot b/helm/ocaml/STATS/daemons.dot similarity index 100% rename from helm/ocaml/daemons.dot rename to helm/ocaml/STATS/daemons.dot diff --git a/helm/ocaml/deps.patch b/helm/ocaml/STATS/deps.patch similarity index 100% rename from helm/ocaml/deps.patch rename to helm/ocaml/STATS/deps.patch diff --git a/helm/ocaml/patch_deps.sh b/helm/ocaml/STATS/patch_deps.sh similarity index 90% rename from helm/ocaml/patch_deps.sh rename to helm/ocaml/STATS/patch_deps.sh index dbdd27c11..d7dd7b3ba 100755 --- a/helm/ocaml/patch_deps.sh +++ b/helm/ocaml/STATS/patch_deps.sh @@ -45,9 +45,9 @@ apply_patch () cp $1 $2 include_loc_stats $2 .stats -apply_patch $2 deps.patch -include_dot_snippet $2 daemons.dot +apply_patch $2 STATS/deps.patch +include_dot_snippet $2 STATS/daemons.dot if [ "$use_clusters" = "yes" ]; then - include_dot_snippet $2 clusters.dot + include_dot_snippet $2 STATS/clusters.dot fi -- 2.39.2