Admin/PIDE/convert
changeset 64385 d072d327b9b2
parent 64380 4b22e1268779
child 64386 e936967c2a06
--- a/Admin/PIDE/convert	Mon Oct 24 18:25:30 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-#!/usr/bin/env bash
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-SUPER="$(cd "$THIS/.."; pwd)"
-
-ISABELLE_REPOS="$(cd "$THIS/../.."; pwd)"
-
-
-## main
-
-FILEMAP="/tmp/filemap$$"
-
-echo "include COPYRIGHT" > "$FILEMAP"
-(
-  cd "$ISABELLE_REPOS"
-  for FILE in $(find src/Pure -name "*.scala")
-  do
-    if grep "Module:.*PIDE" "$FILE" >/dev/null; then
-      if [ "$("${HG:-hg}" status -u -n --color=never "$FILE")" = "" ]; then
-        echo "include $FILE" >> "$FILEMAP"
-        echo "rename $FILE src/$(basename "$FILE")" >> "$FILEMAP"
-      fi
-    fi
-  done
-)
-
-cat "$FILEMAP"
-
-"${HG:-hg}" convert --filemap "$FILEMAP" "$ISABELLE_REPOS" PIDE-repos
-
-rm -f "$FILEMAP"