# HG changeset patch
# User wenzelm
# Date 1346268705 -7200
# Node ID 0febe9e433dd22915073575fcd293d4f4143c9cc
# Parent  96d5e42e5e3ad08f571247bc687b5cf1566e0a1e
discontinued old init_components script, superseded by init_components shell function as explained in README_REPOSITORY;

diff -r 96d5e42e5e3a -r 0febe9e433dd Admin/components_old
--- a/Admin/components_old	Wed Aug 29 21:27:32 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 96d5e42e5e3a -r 0febe9e433dd Admin/init_components
--- a/Admin/init_components	Wed Aug 29 21:27:32 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Author: Florian Haftmann, TU Muenchen
-#
-# init_components - bash source script to initialize components
-# as specified in the Admin directory
-
-while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
-do
-  case "$REPLY" in
-    \#* | "") ;;
-    /*) init_component "$REPLY" ;;
-    *) init_component "$COMPONENT/$REPLY" ;;
-  esac
-done < "$ISABELLE_HOME/Admin/components_old"