aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/settings.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-01-09 17:27:24 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2014-01-09 17:27:24 -0500
commit55d485365f4d52a84d06bc38d6d34b6a47890b57 (patch)
tree67ed3697d7f212b698cdc3cfc8c530c54e5fba64 /src/settings.sig
parentbb567cd6c1490dcabf53a3dd18f1aebd8e3055e0 (diff)
Add 'html5' .urp directive
Diffstat (limited to 'src/settings.sig')
-rw-r--r--src/settings.sig3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/settings.sig b/src/settings.sig
index 847cb5f6..a7a41447 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -265,4 +265,7 @@ signature SETTINGS = sig
val mangleSql : string -> string
val mangleSqlCatalog : string -> string
val mangleSqlTable : string -> string
+
+ val setIsHtml5 : bool -> unit
+ val getIsHtml5 : unit -> bool
end