| author | wenzelm |
| Fri, 09 Jul 2021 21:24:28 +0200 | |
| changeset 73959 | e17f76705cee |
| parent 73161 | 31fbde3baa97 |
| child 79556 | 0631dfc0db07 |
| permissions | -rwxr-xr-x |
|
73161
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
2 |
# |
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
3 |
# java-gui-setup --- platform-specific setup for Java/Swing GUI applications |
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
4 |
|
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
5 |
if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ] |
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
6 |
then |
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
7 |
JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)"
|
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
8 |
JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java"
|
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
9 |
defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || |
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
10 |
defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null |
|
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
diff
changeset
|
11 |
fi |