diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2019-03-16 14:57:25 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2019-03-16 14:57:25 -0400 |
| commit | 18d42a0f0829132803a8c508e1d1cc797c6dbbde (patch) | |
| tree | da17148b671d68916ddd3b9c58d4f36ab965b381 /src | |
| parent | 43666c47b550904e5573e28fab6ba9d2c51ddcd3 (diff) | |
Allow dollar-sign shortcuts for 'file' and 'jsFile' directives
Diffstat (limited to 'src')
| -rw-r--r-- | src/compiler.sml | 4 |
1 files 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 () |