<key name="owner">$(user.name)</key>
<!-- Initial GUI font size. -->
<!-- <key name="font_size">10</key> -->
+ <!-- Perform heavy checks when run interactively (like duplicate check) -->
+ <!-- <key name="do_heavy_checks">false</key> -->
</section>
<section name="db">
<!--
exactly one 'library' db must be specified
exactly one 'legacy' db can be specified
-->
-
- <!-- this snippet is what is used by the helm team, everything on mowgli.
- note that user's tables are named diffrently from library tables, so that
- they can coexists on the same db -->
- <key name="metadata">@DBHOST@ public helm none legacy</key>
+ <!-- The following snippet is used by the helm team
+ note that user's tables are named diffrently from library tables,
+ so they can coexists on the same db -->
+
<key name="metadata">@DBHOST@ matita helm none library</key>
<key name="metadata">@DBHOST@ matita helm none user</key>
- <!-- The following snipset is used by the helm team to publish the matita
- contributions
- <key name="metadata">@DBHOST@ mowgli helm none legacy</key>
- <key name="metadata">@DBHOST@ public helm none library</key>
- <key name="metadata">@DBHOST@ public helm none user</key>
- -->
-
<!-- The following snippet it what you want to use a local sqlite db
and acess remotely to the coq library trought mowgli
<key name="metadata">@DBHOST@ matita helm none legacy</key>
(e.g. the Matita standard library)
"legacy" implies "ro"
-->
- <key name="prefix">
- cic:/matita/
- file:///projects/helm/library/matita_contribs/matita
- ro
- </key>
<key name="prefix">
cic:/matita/
file://$(matita.rt_base_dir)/xml/standard-library/