diff options
Diffstat (limited to 'src/export.sig')
-rw-r--r-- | src/export.sig | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/export.sig b/src/export.sig index 4c46e751..0bbdd1ac 100644 --- a/src/export.sig +++ b/src/export.sig @@ -29,6 +29,7 @@ signature EXPORT = sig datatype effect = ReadOnly + | ReadCookieWrite | ReadWrite datatype export_kind = |