diff -r aeba7bb4f4d4 -r 31fbde3baa97 lib/scripts/java-gui-setup --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/java-gui-setup Tue Jan 19 14:04:31 2021 +0100 @@ -0,0 +1,11 @@ +#!/usr/bin/env bash +# +# java-gui-setup --- platform-specific setup for Java/Swing GUI applications + +if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ] +then + JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" + JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" + defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || + defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null +fi