diff options
author | Adam Chlipala <adam@chlipala.net> | 2011-07-03 12:40:00 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2011-07-03 12:40:00 -0400 |
commit | 765c18f6f32d6e2123ac1aa1c4dcdd522b9faf48 (patch) | |
tree | 57875f0e93a279eeaac3f66eac6372405cdf4b60 /src/compiler.sml | |
parent | 3475f4aa1603ac5793243f6c2766d4cde6cdf6a1 (diff) |
For non-debug builds, leave out source location info in what is shown to user
Diffstat (limited to 'src/compiler.sml')
-rw-r--r-- | src/compiler.sml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/compiler.sml b/src/compiler.sml index 229b40ff..d4f34021 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -324,7 +324,8 @@ fun capitalize "" = "" | capitalize s = str (Char.toUpper (String.sub (s, 0))) ^ String.extract (s, 1, NONE) fun institutionalizeJob (job : job) = - (Settings.setUrlPrefix (#prefix job); + (Settings.setDebug (#debug job); + Settings.setUrlPrefix (#prefix job); Settings.setTimeout (#timeout job); Settings.setHeaders (#headers job); Settings.setScripts (#scripts job); |