comparison src/settings.sml @ 2183:74c762002352

Allow duplicate 'file' directives if paths normalize to same value
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Oct 2015 16:03:56 -0400
parents 3b4a5604ed97
children 14c45a0b6362 1e3ba868f8bf
comparison
equal deleted inserted replaced
2182:d25c42e5d8f4 2183:74c762002352
878 let 878 let
879 val path = OS.Path.concat (!filePath, LoadFromFilename) 879 val path = OS.Path.concat (!filePath, LoadFromFilename)
880 in 880 in
881 case SM.find (!files, Uri) of 881 case SM.find (!files, Uri) of
882 SOME (path', _) => 882 SOME (path', _) =>
883 if path' = path then 883 if OS.Path.mkCanonical path' = OS.Path.mkCanonical path then
884 () 884 ()
885 else 885 else
886 ErrorMsg.error ("Two different files requested for URI " ^ Uri ^ " ( " ^ path' ^ " vs. " ^ path ^ ")") 886 ErrorMsg.error ("Two different files requested for URI " ^ Uri ^ " ( " ^ path' ^ " vs. " ^ path ^ ")")
887 | NONE => 887 | NONE =>
888 let 888 let