From 3256142dc01f7f173289a1910e726b662a877408 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 18 Oct 2015 16:03:56 -0400
Subject: Allow duplicate 'file' directives if paths normalize to same value

---
 src/settings.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/settings.sml')

diff --git a/src/settings.sml b/src/settings.sml
index 10a4af48..bea26103 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -880,7 +880,7 @@ fun addFile {Uri, LoadFromFilename} =
     in
         case SM.find (!files, Uri) of
             SOME (path', _) =>
-            if path' = path then
+            if OS.Path.mkCanonical path' = OS.Path.mkCanonical path then
                 ()
             else
                 ErrorMsg.error ("Two different files requested for URI " ^ Uri ^ " ( " ^ path' ^ " vs. " ^ path ^ ")")
-- 
cgit v1.2.3