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"