]> matita.cs.unibo.it Git - helm.git/commitdiff
removed file:// prefix from local_library key, hopefully it isn't useful
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 28 Apr 2004 14:00:42 +0000 (14:00 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 28 Apr 2004 14:00:42 +0000 (14:00 +0000)
helm/gTopLevel/gTopLevel.conf.xml.sample

index 5b2af4f53b200af5bf3cd904043c7132f13159be..4d5331948d25cd81e8e90d2913d9ba87b52fe2af 100644 (file)
@@ -34,7 +34,7 @@
    <key name="flags"></key>
   </section>
   <section name="local_library">
-    <key name="dir">file://$(users_settings.per_user_work_directory)/objects</key>
+    <key name="dir">$(users_settings.per_user_work_directory)/objects</key>
     <key name="url">$(local_library.dir)</key>
   </section>
   <section name="getter">