refrain from writing to JEDIT_SETTINGS in BUILD_ONLY mode -- relevant for makedist;
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Jan 09 21:24:16 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Jan 09 21:59:53 2013 +0100
@@ -306,12 +306,11 @@
## main
-# perspective
+if [ "$BUILD_ONLY" = false ]; then
+ mkdir -p "$JEDIT_SETTINGS/DockableWindowManager"
-mkdir -p "$JEDIT_SETTINGS/DockableWindowManager"
-
-if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
- cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
+ if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
+ cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
EOF
cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
@@ -323,12 +322,8 @@
</VIEW>
</PERSPECTIVE>
EOF
-fi
-
+ fi
-# main
-
-if [ "$BUILD_ONLY" = false ]; then
if [ "$NO_BUILD" = false ]; then
"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}"
RC="$?"