diff options
| author |  Benjamin Barenblat <bbaren@mit.edu> | 2015-10-24 11:06:31 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@mit.edu> | 2015-10-24 11:06:31 -0400 |
| commit | 7d861ea0debf944cb8e3e38d73a8c0197de574b3 (patch) | |
| tree | ed87d21ffe040bf296d2230c7490abda8e34752c /src/settings.sml | |
| parent | 598756dc69f89cf2dd2b889cad63a7a690ae7ed7 (diff) | |
| parent | cb0109804fdad0dd423bb344446344cdc08c0886 (diff) | |
Merge branch 'upstream' into dfsg_clean20151018+dfsg
Diffstat (limited to 'src/settings.sml')
| -rw-r--r-- | src/settings.sml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/settings.sml b/src/settings.sml index cd2de8a9..10a4af48 100644 --- a/src/settings.sml +++ b/src/settings.sml @@ -883,7 +883,7 @@ fun addFile {Uri, LoadFromFilename} = if path' = path then () else - ErrorMsg.error ("Two different files requested for URI " ^ Uri) + ErrorMsg.error ("Two different files requested for URI " ^ Uri ^ " ( " ^ path' ^ " vs. " ^ path ^ ")") | NONE => let val inf = BinIO.openIn path |