makedist -D retains doc-src component with its "doc" sessions (relevant for testing);
authorwenzelm
Mon, 30 Jul 2012 15:54:17 +0200
changeset 48606 4b6c90e121b1
parent 48605 e777363440d6
child 48607 e24bfa4e3b84
makedist -D retains doc-src component with its "doc" sessions (relevant for testing);
Admin/Release/makedist
--- a/Admin/Release/makedist	Mon Jul 30 15:31:00 2012 +0200
+++ b/Admin/Release/makedist	Mon Jul 30 15:54:17 2012 +0200
@@ -23,6 +23,7 @@
 Usage: $PRG [OPTIONS] [VERSION]
 
   Options are:
+    -D                 retain doc-src component
     -j JEDIT_BUILD     build Isabelle/jEdit via given jedit_build component
     -r RELEASE         proper release with name"
 
@@ -46,12 +47,16 @@
 
 # options
 
+RETAIN_DOC_SRC=""
 RELEASE=""
 ISABELLE_JEDIT_BUILD_HOME=""
 
-while getopts "j:r:" OPT
+while getopts "Dj:r:" OPT
 do
   case "$OPT" in
+    D)
+      RETAIN_DOC_SRC=true
+      ;;
     j)
       ISABELLE_JEDIT_BUILD_HOME="$OPTARG"
       ;;
@@ -147,6 +152,10 @@
 
 perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings
 
+if [ -n "$RETAIN_DOC_SRC" ]; then
+  cp -a doc-src doc-src.orig
+fi
+
 ./Admin/build all || fail "Failed to build distribution"
 
 if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
@@ -165,6 +174,10 @@
 rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
 rm -rf doc-src
 
+if [ -n "$RETAIN_DOC_SRC" ]; then
+  mv doc-src.orig doc-src
+fi
+
 mkdir -p contrib
 cat >contrib/README <<EOF
 This directory contains add-on components that contribute to the main