aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/g_ground.mlg1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 9d208e1c86..930801f6fd 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -36,7 +36,6 @@ let ground_depth=ref 3
let ()=
let gdopt=
{ optdepr=false;
- optname="Firstorder Depth";
optkey=["Firstorder";"Depth"];
optread=(fun ()->Some !ground_depth);
optwrite=