diff options
| author |  Ziv Scully <ziv@mit.edu> | 2015-09-12 17:11:33 -0400 |
|---|---|---|
| committer | Ziv Scully <ziv@mit.edu> | 2015-09-12 17:11:33 -0400 |
| commit | 6aadea0202190d17a35f289f984eb19ec8116672 (patch) | |
| tree | e981fc563a09eab62b50f3ba52eaa01cac157f3e /src/settings.sml | |
| parent | 5c4c302aea71f47679e8d8b4197f869355b2180a (diff) | |
| parent | 03f1d80a665c4de6fd83ff6dc9399dda97838efa (diff) | |
Merge.
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 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 |