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 fc55511d..ff99bf13 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -887,7 +887,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