# HG changeset patch
# User berghofe
# Date 1340960357 -7200
# Node ID 6404816632f76926ffa92db155541ffd4d71167c
# Parent  e825bbf49363e84df217b4c1709fd472c2c4b768# Parent  1bee47c0c278ed3124887103a2c9d1a8f76f0af3
merged

diff -r e825bbf49363 -r 6404816632f7 Admin/components.x86-linux
--- a/Admin/components.x86-linux	Fri Jun 29 10:08:41 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-contrib/jdk-6u31_x86-linux
diff -r e825bbf49363 -r 6404816632f7 Admin/components.x86_64-linux
--- a/Admin/components.x86_64-linux	Fri Jun 29 10:08:41 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-contrib/jdk-6u31_x86_64-linux
diff -r e825bbf49363 -r 6404816632f7 Admin/init_components
--- a/Admin/init_components	Fri Jun 29 10:08:41 2012 +0200
+++ b/Admin/init_components	Fri Jun 29 10:59:17 2012 +0200
@@ -16,14 +16,11 @@
   fi
 }
 
-for COMPONENTS_FILE in "${ISABELLE_HOME}/Admin/components" "${ISABELLE_HOME}/Admin/components.${ML_PLATFORM}"
+while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
 do
-  while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
-  do
-    case "${REPLY}" in
-      \#* | "") ;;
-      /*) init_component_liberal "${REPLY}" ;;
-      *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
-    esac
-  done < "${COMPONENTS_FILE}"
-done
+  case "${REPLY}" in
+    \#* | "") ;;
+    /*) init_component_liberal "${REPLY}" ;;
+    *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
+  esac
+done < "${ISABELLE_HOME}/Admin/components"