aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/export.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-23 14:10:10 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-23 14:10:10 -0400
commit1c5416512d92309bb3f6a98f439edaf5a21d2318 (patch)
tree5f9043f30674edd2b558719bbd85211d45b02297 /src/export.sml
parent369f5592adc342fc7e2436fa14ec6671c747685e (diff)
Only use cookie signatures when cookies might be read
Diffstat (limited to 'src/export.sml')
-rw-r--r--src/export.sml4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/export.sml b/src/export.sml
index 8e3e3331..ad604e16 100644
--- a/src/export.sml
+++ b/src/export.sml
@@ -25,13 +25,14 @@
* POSSIBILITY OF SUCH DAMAGE.
*)
-structure Export = struct
+structure Export :> EXPORT = struct
open Print.PD
open Print
datatype effect =
ReadOnly
+ | ReadCookieWrite
| ReadWrite
datatype export_kind =
@@ -42,6 +43,7 @@ datatype export_kind =
fun p_effect ef =
case ef of
ReadOnly => string "r"
+ | ReadCookieWrite => string "rcw"
| ReadWrite => string "rw"
fun p_export_kind ck =