summaryrefslogtreecommitdiff
path: root/src/settings.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/settings.sml')
-rw-r--r--src/settings.sml2
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