src/Tools/jEdit/makedist
changeset 41513 0ffd5ea44078
parent 37355 1255ba99ed1e
child 41514 917f1a4fbc77
equal deleted inserted replaced
41512:8445396e1e39 41513:0ffd5ea44078
    64 
    64 
    65 
    65 
    66 # target name
    66 # target name
    67 
    67 
    68 [ -z "$JEDIT_HOME" ] && fail "Unknown JEDIT_HOME"
    68 [ -z "$JEDIT_HOME" ] && fail "Unknown JEDIT_HOME"
       
    69 [ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
    69 
    70 
    70 VERSION=$(basename "$JEDIT_HOME")
    71 VERSION="$(basename "$JEDIT_HOME")_Isabelle-$("$ISABELLE_TOOL" version -i)"
    71 JEDIT="jedit-${VERSION}"
    72 JEDIT="jedit-${VERSION}"
    72 
    73 
    73 rm -rf "$JEDIT" jedit
    74 rm -rf "$JEDIT" jedit
    74 mkdir "$JEDIT"
    75 mkdir "$JEDIT"
    75 
    76