diff options
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -217,7 +217,7 @@ let tclose () = Glue.atom(Ppcmd_close_tbox) (* Opening and closed of tags *) let open_tag t = Glue.atom(Ppcmd_open_tag t) let close_tag () = Glue.atom(Ppcmd_close_tag) - +let tag t s = open_tag t ++ s ++ close_tag () let eval_ppcmds l = l (* In new syntax only double quote char is escaped by repeating it *) |