aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/cjr_print.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-30 17:15:14 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-30 17:15:14 -0400
commit2307ccdcc5eb4ddfe719ddcbea999f7705ec79c3 (patch)
tree4be9b76a5e655b9f28be47710cc47e600a369a14 /src/cjr_print.sig
parentdb2f1f208afef9110d8a5796a2325928a92b62cc (diff)
C FFI compiler options
Diffstat (limited to 'src/cjr_print.sig')
-rw-r--r--src/cjr_print.sig2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/cjr_print.sig b/src/cjr_print.sig
index d7fb21a0..baef005e 100644
--- a/src/cjr_print.sig
+++ b/src/cjr_print.sig
@@ -36,6 +36,4 @@ signature CJR_PRINT = sig
val p_sql : CjrEnv.env -> Cjr.file Print.printer
val debug : bool ref
-
- val timeout : int ref
end