CIC files are now processed one by one once given the list of their

[helm.git] / helm / metadata / create / Makefile

diff --git a/helm/metadata/create/Makefile b/helm/metadata/create/Makefile
index ac242589d4137913c93a146b0201ff2e3185c204..aebe7233e75302d6ffdc856d7f92314237b897ab 100644 (file)
--- a/helm/metadata/create/Makefile
+++ b/helm/metadata/create/Makefile
@@ -1,67 +1,8 @@
-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)