Mercurial > urweb

changeset 1336:7eefe077075a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix merging of prefix settings
author Adam Chlipala <adam@chlipala.net>
date Sun, 12 Dec 2010 10:57:41 -0500
parents 79557535b843
children b4b5788b20ea
files src/compiler.sml
diffstat 1 files changed, 1 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/compiler.sml	Sun Dec 12 10:44:19 2010 -0500
+++ b/src/compiler.sml	Sun Dec 12 10:57:41 2010 -0500
@@ -617,11 +617,7 @@
                                               (("", ""), ""))
                             in
                                 case cmd of
-                                    "prefix" =>
-                                    (case !prefix of
-                                         NONE => ()
-                                       | SOME _ => ErrorMsg.error "Duplicate 'prefix' directive";
-                                     prefix := SOME arg)
+                                    "prefix" => prefix := SOME arg
                                   | "database" =>
                                     (case !database of
                                          NONE => database := SOME arg