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"