From: Enrico Tassi Date: Mon, 12 Oct 2009 14:27:36 +0000 (+0000) Subject: new standard library inside path X-Git-Tag: make_still_working~3337 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa067dece23a0e3dff167f7e1c6d35f067451ec2;p=helm.git new standard library inside path --- diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index 544d0fd70..7c42dc818 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -285,6 +285,7 @@ endif ln -fs matita $(WHERE)/$$p;\ done $(H)cp -a library/ $(WHERE)/ma/standard-library + $(H)cp -a nlibrary/ $(WHERE)/ma/new-standard-library $(H)touch install_preliminaries.stamp diff --git a/helm/software/matita/buildTimeConf.ml.in b/helm/software/matita/buildTimeConf.ml.in index 6f693a138..45b75736e 100644 --- a/helm/software/matita/buildTimeConf.ml.in +++ b/helm/software/matita/buildTimeConf.ml.in @@ -51,6 +51,8 @@ let matita_conf = runtime_base_dir ^ "/matita.conf.xml" let closed_xml = runtime_base_dir ^ "/closed.xml" let gtkmathview_conf = runtime_base_dir ^ "/gtkmathview.matita.conf.xml" let stdlib_dir_devel = runtime_base_dir ^ "/library" +let new_stdlib_dir_devel = runtime_base_dir ^ "/nlibrary" let stdlib_dir_installed = runtime_base_dir ^ "/ma/standard-library" +let new_stdlib_dir_installed = runtime_base_dir ^ "/ma/new-standard-library" let help_dir = runtime_base_dir ^ "/help" diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 3291cbc33..70125f54c 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -176,7 +176,10 @@ let parse_cmdline init_status = let includes = ref [] in let default_includes = [ BuildTimeConf.stdlib_dir_devel; - BuildTimeConf.stdlib_dir_installed ; ] + BuildTimeConf.stdlib_dir_installed ; + BuildTimeConf.new_stdlib_dir_devel; + BuildTimeConf.new_stdlib_dir_installed ; + ] in let absolutize s = if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s