Admin/PIDE/convert
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 53498 05313b45a5ae
permissions -rwxr-xr-x
use E 1.8's auto scheduler option
     1 #!/usr/bin/env bash
     2 
     3 THIS="$(cd "$(dirname "$0")"; pwd)"
     4 SUPER="$(cd "$THIS/.."; pwd)"
     5 
     6 ISABELLE_REPOS="$(cd "$THIS/../.."; pwd)"
     7 
     8 
     9 ## main
    10 
    11 FILEMAP="/tmp/filemap$$"
    12 
    13 echo "include COPYRIGHT" > "$FILEMAP"
    14 (
    15   cd "$ISABELLE_REPOS"
    16   for FILE in $(find src/Pure -name "*.scala")
    17   do
    18     if grep "Module:.*PIDE" "$FILE" >/dev/null; then
    19       if [ "$("${HG:-hg}" status -u -n --color=never "$FILE")" = "" ]; then
    20         echo "include $FILE" >> "$FILEMAP"
    21         echo "rename $FILE src/$(basename "$FILE")" >> "$FILEMAP"
    22       fi
    23     fi
    24   done
    25 )
    26 
    27 cat "$FILEMAP"
    28 
    29 "${HG:-hg}" convert --filemap "$FILEMAP" "$ISABELLE_REPOS" PIDE-repos
    30 
    31 rm -f "$FILEMAP"