comparison 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
comparison
equal deleted inserted replaced
2248:e09c3dc102ef 2249:c05851bf7861
885 case SM.find (!files, Uri) of 885 case SM.find (!files, Uri) of
886 SOME (path', _) => 886 SOME (path', _) =>
887 if path' = path then 887 if path' = path then
888 () 888 ()
889 else 889 else
890 ErrorMsg.error ("Two different files requested for URI " ^ Uri) 890 ErrorMsg.error ("Two different files requested for URI " ^ Uri ^ " ( " ^ path' ^ " vs. " ^ path ^ ")")
891 | NONE => 891 | NONE =>
892 let 892 let
893 val inf = BinIO.openIn path 893 val inf = BinIO.openIn path
894 in 894 in
895 files := SM.insert (!files, 895 files := SM.insert (!files,