src/Tools/jEdit/lib/Tools/jedit
changeset 73161 31fbde3baa97
parent 72248 71378e7d148e
child 73652 d5c3eee7da74
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Jan 19 13:48:53 2021 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Jan 19 14:04:31 2021 +0100
@@ -408,6 +408,8 @@
 
 if [ "$BUILD_ONLY" = false ]
 then
+  "$ISABELLE_HOME/lib/scripts/java-gui-setup"
+
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
     JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
   export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"