equal
deleted
inserted
replaced
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 \ |
|
15 -p /bin/bash \ |
14 -p /bin/bash \ |
16 -c "$THIS/script" \ |
15 -c "$THIS/script" \ |
17 -o None \ |
16 -o None \ |
18 -f "$COCOADIALOG_APP" \ |
17 -f "$COCOADIALOG_APP" \ |
19 "$PWD/Isabelle.app" |
18 "$PWD/Isabelle.app" |