diff options
Diffstat (limited to 'contrib/first-order/g_ground.ml4')
| -rw-r--r-- | contrib/first-order/g_ground.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 index 059ca69a6a..2e8929c55e 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -25,7 +25,7 @@ let ground_depth=ref 5 let _= let gdopt= - { optsync=false; + { optsync=true; optname="ground_depth"; optkey=SecondaryTable("Ground","Depth"); optread=(fun ()->Some !ground_depth); |