# HG changeset patch
# User wenzelm
# Date 1345218506 -7200
# Node ID ac976e51cb678e8c9148a9f663376c376c59f80e
# Parent  90fe0798b83a920abb4ca7e7ce7e5eccb8ec2b06
renamed components to components_old, to make room for some directory of the same name;

diff -r 90fe0798b83a -r ac976e51cb67 Admin/components
--- a/Admin/components	Fri Aug 17 15:05:57 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-#contributed components
-contrib/cvc3-2.4.1
-contrib/e-1.5
-contrib/hol-light-bundle-0.5-126
-contrib/kodkodi-1.2.16
-contrib/spass-3.8ds
-contrib/vampire-1.0
-contrib/yices-1.0.28
-contrib/z3-4.0
-contrib/jdk-7u6
-contrib/scala-2.9.2
-contrib/jedit_build-20120813
-
diff -r 90fe0798b83a -r ac976e51cb67 Admin/components_old
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components_old	Fri Aug 17 17:48:26 2012 +0200
@@ -0,0 +1,13 @@
+#contributed components
+contrib/cvc3-2.4.1
+contrib/e-1.5
+contrib/hol-light-bundle-0.5-126
+contrib/kodkodi-1.2.16
+contrib/spass-3.8ds
+contrib/vampire-1.0
+contrib/yices-1.0.28
+contrib/z3-4.0
+contrib/jdk-7u6
+contrib/scala-2.9.2
+contrib/jedit_build-20120813
+
diff -r 90fe0798b83a -r ac976e51cb67 Admin/init_components
--- a/Admin/init_components	Fri Aug 17 15:05:57 2012 +0200
+++ b/Admin/init_components	Fri Aug 17 17:48:26 2012 +0200
@@ -12,4 +12,4 @@
     /*) init_component "$REPLY" ;;
     *) init_component "$COMPONENT/$REPLY" ;;
   esac
-done < "$ISABELLE_HOME/Admin/components"
+done < "$ISABELLE_HOME/Admin/components_old"