diff options
Diffstat (limited to 'ide/ideproof.ml')
| -rw-r--r-- | ide/ideproof.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/ideproof.ml b/ide/ideproof.ml index 700b5a729..3d86f52c6 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -7,8 +7,6 @@ (************************************************************************) -(* $Id$ *) - (* tag is the tag to be hooked, item is the item covered by this tag, make_menu * * is the template for building menu if needed, sel_cb is the callback if * there |