aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/cjr.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-03-10 10:44:26 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-03-10 10:44:26 -0400
commitdb7cd221444afce64803e66594d56dc8e7a0843c (patch)
treeda2a0ab3f900743c5d1aaa01d30b665aa858f021 /src/cjr.sml
parentaed3aa32e62846a16da55fc7be4cecba92ed5e2b (diff)
Avoid any JavaScript when pages don't need it; update demo prose
Diffstat (limited to 'src/cjr.sml')
-rw-r--r--src/cjr.sml6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/cjr.sml b/src/cjr.sml
index a38a1b0d..688326e4 100644
--- a/src/cjr.sml
+++ b/src/cjr.sml
@@ -113,6 +113,10 @@ datatype decl' =
withtype decl = decl' located
-type file = decl list * (Core.export_kind * string * int * typ list * typ) list
+datatype sidedness =
+ ServerOnly
+ | ServerAndClient
+
+type file = decl list * (Core.export_kind * string * int * typ list * typ * sidedness) list
end