diff src/settings.sml @ 2249:c05851bf7861

Merge.
author Ziv Scully <ziv@mit.edu>
date Sat, 12 Sep 2015 17:11:33 -0400
parents a07b91fa71db 3b4a5604ed97
children a647a1560628
line wrap: on
line diff
--- a/src/settings.sml	Sat Aug 15 23:08:37 2015 -0700
+++ b/src/settings.sml	Sat Sep 12 17:11:33 2015 -0400
@@ -887,7 +887,7 @@
             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