X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmetadata%2Fcreate%2FMakefile;h=a8ce85cbb339704bc3e769e958f09427be943391;hb=d42f916052e67304e8b46e537b9a4bbaf2c2607e;hp=ac242589d4137913c93a146b0201ff2e3185c204;hpb=c59f43de7aaacf1901c68dcfbcac6fe759759a29;p=helm.git

diff --git a/helm/metadata/create/Makefile b/helm/metadata/create/Makefile
index ac242589d..a8ce85cbb 100644
--- a/helm/metadata/create/Makefile
+++ b/helm/metadata/create/Makefile
@@ -1,73 +1,14 @@
-marcello_THEORIES_OK = \
- cic:/Coq/Arith/ \
- cic:/Coq/Bool/ \
- cic:/Coq/Init/ \
-\
- cic:/Coq/IntMap/Adalloc/ \
- cic:/Coq/IntMap/Addec/ \
- cic:/Coq/IntMap/Addr/ \
- cic:/Coq/IntMap/Adist/ \
- cic:/Coq/IntMap/Fset/ \
- cic:/Coq/IntMap/Lsort/ \
- cic:/Coq/IntMap/Map/ \
- cic:/Coq/IntMap/Mapaxioms/ \
- cic:/Coq/IntMap/Mapc/ \
- cic:/Coq/IntMap/Mapcanon/ \
- cic:/Coq/IntMap/Mapcard/ \
- cic:/Coq/IntMap/Mapfold/ \
- cic:/Coq/IntMap/Mapiter/ \
- cic:/Coq/IntMap/Maplists/ \
- cic:/Coq/IntMap/Mapsubset/ \
-\
- cic:/Coq/Lists/ \
- cic:/Coq/Logic/ \
-\
- cic:/Coq/Reals/R_Ifp/ \
- cic:/Coq/Reals/Raxioms/ \
- cic:/Coq/Reals/Rbase/ \
- cic:/Coq/Reals/Rbasic_fun/ \
- cic:/Coq/Reals/Rdefinitions/ \
- cic:/Coq/Reals/Rderiv/ \
- cic:/Coq/Reals/Rfunctions/ \
- cic:/Coq/Reals/Rlimit/ \
- cic:/Coq/Reals/Rseries/ \
- cic:/Coq/Reals/Rsyntax/ \
- cic:/Coq/Reals/Rtrigo_fun/ \
- cic:/Coq/Reals/TypeSyntax/ \
-\
- cic:/Coq/Relations/ \
- cic:/Coq/Sets/ \
- cic:/Coq/Wellfounded/ \
-\
- cic:/Coq/ZArith/Wf_Z/ \
- cic:/Coq/ZArith/ZArith_dec/ \
- cic:/Coq/ZArith/Zmisc/ \
- cic:/Coq/ZArith/Zsyntax/ \
- cic:/Coq/ZArith/auxiliary/ \
- cic:/Coq/ZArith/fast_integer/ \
- cic:/Coq/ZArith/zarith_aux/ \
-\
- cic:/Coq/correctness/ \
- cic:/Coq/field/ \
- cic:/Coq/fourier/ \
-\
- cic:/Coq/omega/Zcomplements/ \
- cic:/Coq/omega/Zlogarithm/ \
- cic:/Coq/omega/Zpower/ \
-\
- cic:/Coq/ring/ \
-
 marcello:
-	time ./mywget.pl $($@_THEORIES_OK)
+	time for i in `cat pluto` ; do ./mywget.pl $$i ; done
 
 rdf:
-	./split.pl output/*
+	find output -type f -exec ./split.pl {} \;
 	find rdf -type f -exec ./fix_rdf.pl {} \;
 	(cd rdf ; ../mkindex.sh)
 
 .PHONY: clean rdf clean-rdf
 clean:
-	rm -f output/*
+	find output -type f -exec rm {} \;
 
 clean-rdf:
 	rm -rf rdf/*