summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAdam Chlipala <adam@chlipala.net>2020-01-10 14:49:05 -0500
committerAdam Chlipala <adam@chlipala.net>2020-01-10 14:49:05 -0500
commit0bb63dca9409308491070d94a0436ad73f81b9e0 (patch)
tree75735498de69779c564cabfb7705837e9b69553b
parent7dc460aece761171338fe61f1a6d601e3d0b6e62 (diff)
At compile time, allow '#' as a URL
-rw-r--r--src/mono_opt.sml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/mono_opt.sml b/src/mono_opt.sml
index cc85f05b..7e737e44 100644
--- a/src/mono_opt.sml
+++ b/src/mono_opt.sml
@@ -161,7 +161,7 @@ fun unAs s =
doChars (String.explode s, [])
end
-fun checkUrl s = CharVector.all Char.isGraph s andalso Settings.checkUrl s
+fun checkUrl s = CharVector.all Char.isGraph s andalso (s = "#" orelse Settings.checkUrl s)
val checkData = CharVector.all (fn ch => Char.isAlphaNum ch
orelse ch = #"_"
orelse ch = #"-")