| changeset 48848 | ae7429d66b1e |
| parent 48785 | 1e384f729045 |
| child 49175 | eab51f249c70 |
--- 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