From 18d42a0f0829132803a8c508e1d1cc797c6dbbde Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 16 Mar 2019 14:57:25 -0400
Subject: Allow dollar-sign shortcuts for 'file' and 'jsFile' directives

---
 src/compiler.sml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/compiler.sml b/src/compiler.sml
index 7099effc..aad5ce8c 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -953,7 +953,7 @@ fun parseUrp' accLibs fname =
                                           uri :: fname :: rest =>
                                           (Settings.setFilePath thisPath;
                                            Settings.addFile {Uri = uri,
-                                                             LoadFromFilename = fname,
+                                                             LoadFromFilename = pathify fname,
                                                              MimeType = case rest of
                                                                             [] => NONE
                                                                           | [ty] => SOME ty
@@ -964,7 +964,7 @@ fun parseUrp' accLibs fname =
 
                                    | "jsFile" =>
                                      (Settings.setFilePath thisPath;
-                                      Settings.addJsFile arg)
+                                      Settings.addJsFile (pathify arg))
 
                                    | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'");
                                  read ()
-- 
cgit v1.2.3