projects / tatoo.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f93c005) | patch
Simply use String.make for Pretty.padding and Pretty.line, since it's
authorKim Nguyễn <kn@lri.fr>
Mon, 4 Mar 2013 17:53:38 +0000 (18:53 +0100)
committerKim Nguyễn <kn@lri.fr>
Mon, 4 Mar 2013 18:02:02 +0000 (19:02 +0100)
commitd16314f40989a63bbd1119a9701fa44e336599ff
tree6d095fb4ef97c23f51e7c45fac6972ef65afd5c3tree | snapshot
parentf93c0057cfca9610e40f9214b286174a041e422acommit | diff
Simply use String.make for Pretty.padding and Pretty.line, since it's
only used in places where performance is not critical.
src/utils/pretty.ml diff | blob | history
Tree Automata TOOlkit