]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/metadata/create_V7_mowgli/mkindex.sh
New version for the new DTD.
[helm.git] / helm / metadata / create_V7_mowgli / mkindex.sh
diff --git a/helm/metadata/create_V7_mowgli/mkindex.sh b/helm/metadata/create_V7_mowgli/mkindex.sh
new file mode 100755 (executable)
index 0000000..3a814ba
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/bash
+
+echo `find . -name "*.xml"` | ../uris_of_filenames.pl $1 > rdf_index.txt
+echo `find . -name "*.xml.gz"` | ../uris_of_filenames.pl $1 -gz >> rdf_index.txt