# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1292169461 18000
# Node ID 7eefe077075a57c3c87022a19113dd294c1be6e0
# Parent  79557535b843eab9a3d0f47a9843c0bd917d6bf1
Fix merging of prefix settings

diff -r 79557535b843 -r 7eefe077075a src/compiler.sml
--- 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