Admin/MacOS/mk
changeset 29151 fa5224eb28a5
parent 29136 de5b29c25af9
child 29154 32b13b953e3a
equal deleted inserted replaced
29150:8af5ee47f30c 29151:fa5224eb28a5
     9 
     9 
    10 "$PLATYPUS_APP/Contents/Resources/platypus" \
    10 "$PLATYPUS_APP/Contents/Resources/platypus" \
    11   -a Isabelle -u Isabelle \
    11   -a Isabelle -u Isabelle \
    12   -I "de.tum.in.isabelle" \
    12   -I "de.tum.in.isabelle" \
    13   -i "$THIS/isabelle.icns" \
    13   -i "$THIS/isabelle.icns" \
    14   -D -X .thy \
    14   -D -X thy \
    15   -p /bin/bash \
    15   -p /bin/bash \
    16   -c "$THIS/script" \
    16   -c "$THIS/script" \
    17   -o None \
    17   -o None \
    18   -f "$COCOADIALOG_APP" \
    18   -f "$COCOADIALOG_APP" \
    19   "$THIS/Isabelle.app"
    19   Isabelle.app