# HG changeset patch
# User wenzelm
# Date 1538846112 -7200
# Node ID 80494b8323fa841e0b3cd2cd1d9820dc45e0b4b2
# Parent  40df889478505b2d1db9d4dc88bc72fc60517e4b
updated to jdk-11: jre is only a symlink to jdk;

diff -r 40df88947850 -r 80494b8323fa Admin/lib/Tools/makedist_bundle
--- 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/."