summaryrefslogtreecommitdiff
path: root/src/elaborate.sig
diff options
context:
space:
mode:
Diffstat (limited to 'src/elaborate.sig')
-rw-r--r--src/elaborate.sig1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 18e6c3b4..b4a4da88 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -42,5 +42,6 @@ signature ELABORATE = sig
* early phase. *)
val incremental : bool ref
+ val verbose : bool ref
end