equal
deleted
inserted
replaced
|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # java-gui-setup --- platform-specific setup for Java/Swing GUI applications |
|
4 |
|
5 if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ] |
|
6 then |
|
7 JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" |
|
8 JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" |
|
9 defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || |
|
10 defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null |
|
11 fi |