diff options
Diffstat (limited to 'ide/tags.ml')
| -rw-r--r-- | ide/tags.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/tags.ml b/ide/tags.ml index 842ac53bc..3b407a19d 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - let make_tag (tt:GText.tag_table) ~name prop = let new_tag = GText.tag ~name () in |