# HG changeset patch
# User wenzelm
# Date 1357765193 -3600
# Node ID 69810ebe120fbe32baf1e8774ca87a7418cc6980
# Parent  a62d048e62135be0b606589e54d3b352a2337ad2
refrain from writing to JEDIT_SETTINGS in BUILD_ONLY mode -- relevant for makedist;

diff -r a62d048e6213 -r 69810ebe120f 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="$?"