diff src/settings.sml @ 1637:e374b6b8ab38

Allow .urp libraries to set prefix
author Adam Chlipala <adam@chlipala.net>
date Sat, 17 Dec 2011 13:10:23 -0500
parents deeeb036c8ed
children ac141fbb313a
line wrap: on
line diff
--- a/src/settings.sml	Sat Dec 17 12:01:31 2011 -0500
+++ b/src/settings.sml	Sat Dec 17 13:10:23 2011 -0500
@@ -27,12 +27,14 @@
 
 structure Settings :> SETTINGS = struct
 
+val urlPrefixFull = ref "/"
 val urlPrefix = ref "/"
 val urlPrePrefix = ref ""
 val timeout = ref 0
 val headers = ref ([] : string list)
 val scripts = ref ([] : string list)
 
+fun getUrlPrefixFull () = !urlPrefixFull
 fun getUrlPrefix () = !urlPrefix
 fun getUrlPrePrefix () = !urlPrePrefix
 fun setUrlPrefix p =
@@ -62,6 +64,7 @@
             else
                 ("", prefix)
     in
+        urlPrefixFull := p;
         urlPrePrefix := prepre;
         urlPrefix := prefix
     end