support for platform-specific components
authorhaftmann
Tue, 26 Jun 2012 22:25:36 +0200
changeset 48152 f06697f776b0
parent 48151 a80595d4f850
child 48153 210043eb4c88
support for platform-specific components
Admin/components.x86-linux
Admin/components.x86_64-linux
Admin/init_components
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components.x86-linux	Tue Jun 26 22:25:36 2012 +0200
@@ -0,0 +1,1 @@
+contrib/jdk-6u31_x86-linux
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components.x86_64-linux	Tue Jun 26 22:25:36 2012 +0200
@@ -0,0 +1,1 @@
+contrib/jdk-6u31_x86_64-linux
--- a/Admin/init_components	Tue Jun 26 22:23:28 2012 +0200
+++ b/Admin/init_components	Tue Jun 26 22:25:36 2012 +0200
@@ -16,11 +16,14 @@
   fi
 }
 
-while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
+for COMPONENTS_FILE in "${ISABELLE_HOME}/Admin/components" "${ISABELLE_HOME}/Admin/components.${ML_PLATFORM}"
 do
-  case "${REPLY}" in
-    \#* | "") ;;
-    /*) init_component_liberal "${REPLY}" ;;
-    *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
-  esac
-done < "${ISABELLE_HOME}/Admin/components"
+  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