--- a/Admin/lib/Tools/makedist_bundle Sat Oct 06 17:37:09 2018 +0200
+++ b/Admin/lib/Tools/makedist_bundle Sat Oct 06 19:15:12 2018 +0200
@@ -158,37 +158,11 @@
}
-# purge jdk -- keep only jre
-
-function purge_jdk
-{
- local DIR="contrib/jdk/$1"
- (
- cd "$ISABELLE_TARGET"
- if [ -d "$DIR/jre" ]; then
- for X in "$DIR"/*
- do
- case "$X" in
- */jre) ;;
- *)
- echo "removing $X"
- rm -rf "$X"
- ;;
- esac
- done
- else
- fail "Bad JDK directory: \"$DIR\""
- fi
- )
-}
-
-
# platform-specific setup (inside archive)
case "$PLATFORM_FAMILY" in
linux)
purge_target 'contrib -name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
- purge_jdk "x86_64-linux"
(
init_component "$JEDIT_HOME"
@@ -221,7 +195,6 @@
;;
macos)
purge_target 'contrib -name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
- purge_jdk "x86_64-darwin/Contents/Home"
mv "$ISABELLE_TARGET/contrib/macos_app" "$TMP/."
perl -pi \
@@ -233,7 +206,6 @@
;;
windows)
purge_target 'contrib -name "x86*-linux" -o -name "x86*-darwin" -o -name "x86-cygwin"'
- purge_jdk "x86_64-windows"
mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/."