# HG changeset patch
# User wenzelm
# Date 1345223335 -7200
# Node ID ae7429d66b1e09532e527ca655e7af53521729b7
# Parent  06e8cb8f3f616e8b1c8493625b1abb3c3018b318
updated to new init_components, hoping that mira can digest that;

diff -r 06e8cb8f3f61 -r ae7429d66b1e Admin/mira.py
--- a/Admin/mira.py	Fri Aug 17 19:07:14 2012 +0200
+++ b/Admin/mira.py	Fri Aug 17 19:08:55 2012 +0200
@@ -39,7 +39,9 @@
 
 Z3_NON_COMMERCIAL="yes"
 
-source "${ISABELLE_HOME}/Admin/init_components"
+init_components "$COMPONENT/contrib" "$ISABELLE_HOME/Admin/components/main"
+init_components "$COMPONENT/contrib" "$ISABELLE_HOME/Admin/components/optional"
+init_components "$COMPONENT/contrib" "$ISABELLE_HOME/Admin/components/nonfree"
 
 ''' + more_settings