Admin/Isabelle_app/build
changeset 73705 ac07f6be27ea
parent 73192 e7437085e589
equal deleted inserted replaced
73704:7c7a59b76528 73705:ac07f6be27ea
     1 #!/usr/bin/env bash
     1 #!/usr/bin/env bash
     2 
     2 
     3 set -e
     3 set -e
     4 
     4 
       
     5 unset CDPATH
     5 THIS="$(cd "$(dirname "$0")"; pwd)"
     6 THIS="$(cd "$(dirname "$0")"; pwd)"
     6 cd "$THIS"
     7 cd "$THIS"
     7 
     8 
     8 source "../../lib/scripts/isabelle-platform"
     9 source "../../lib/scripts/isabelle-platform"
     9 
    10