aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 92a782d965..29e4b02e3f 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -34,6 +34,8 @@ module AsyncOpts : sig
async_proofs_tac_error_resilience : tac_error_filter;
async_proofs_cmd_error_resilience : bool;
async_proofs_delegation_threshold : float;
+
+ async_proofs_worker_priority : CoqworkmgrApi.priority;
}
val default_opts : stm_opt