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 2e8929c55e..95488265b5 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -26,7 +26,7 @@ let ground_depth=ref 5 let _= let gdopt= { optsync=true; - optname="ground_depth"; + optname="Ground Depth"; optkey=SecondaryTable("Ground","Depth"); optread=(fun ()->Some !ground_depth); optwrite= |