src/Pure/General/length.scala
Tue, 20 Dec 2016 17:09:40 +0100 wenzelm added option -T: text length encoding;
Tue, 20 Dec 2016 16:08:02 +0100 wenzelm more systematic text length wrt. encoding;
less more (0) tip