Mercurial > urweb
changeset 1336:7eefe077075a
Fix merging of prefix settings
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 12 Dec 2010 10:57:41 -0500 (2010-12-12) |
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