refrain from writing to JEDIT_SETTINGS in BUILD_ONLY mode -- relevant for makedist;
authorwenzelm
Wed, 09 Jan 2013 21:59:53 +0100
changeset 50795 69810ebe120f
parent 50794 a62d048e6213
child 50796 2d68df7ed89d
refrain from writing to JEDIT_SETTINGS in BUILD_ONLY mode -- relevant for makedist;
src/Tools/jEdit/lib/Tools/jedit
--- 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="$?"