aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.ml
diff options
context:
space:
mode:
authorEnrico Tassi2016-06-07 09:57:09 -0400
committerEnrico Tassi2016-06-07 09:57:09 -0400
commit4dcd50dd2767c60f8f773fb4ca1c3d4bc68819c8 (patch)
tree424b1f5391e453d5e7964071fac9ec6aa99e9be9 /lib/flags.ml
parent7a9462ce9a3d70ca43c363da3a0782f59c16a120 (diff)
Documentation
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index e78fa7c0c9..16996c144b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -69,7 +69,7 @@ let priority_of_string = function
| "high" -> High
| _ -> raise (Invalid_argument "priority_of_string")
type tac_error_filter = [ `None | `Only of string list | `All ]
-let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "proof-block" ])
+let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ])
let async_proofs_cmd_error_resilience = ref true
let async_proofs_is_worker () =