PatR 1ec6e6f96b
Guidebook.mn streamlining ...
Set up variable 'fF' once and use it to conditionalize between
fixed-width font Guidebook.txt and proportional-width font
Guidebook.ps instead of making the width comparison of 'f' and 'F'
each time. There are four instances where it is used; three that
suppress some indentation for the plain text output and one that
manually wraps a couple of long lines for it.
This change shouldn't produce different output from before (last
night) and doesn't need any corresponding change in Guidebook.tex.
2020-02-12 11:43:25 -08:00
2018-11-11 10:29:52 -05:00
2019-01-08 13:56:59 -08:00
2019-11-03 17:59:39 -08:00
2018-04-25 16:54:50 -04:00
2020-01-14 12:01:30 -05:00
2018-09-21 16:36:38 -04:00
2018-09-21 18:12:42 -07:00
2018-09-21 18:12:42 -07:00
2018-09-21 14:57:12 -04:00
2018-04-25 16:54:50 -04:00
2018-09-21 14:57:12 -04:00
2018-09-21 14:57:12 -04:00
2018-09-21 18:12:42 -07:00
2018-09-21 14:57:12 -04:00
2018-09-21 14:57:12 -04:00
2018-09-21 14:57:12 -04:00
2018-09-21 14:57:12 -04:00
2018-09-21 18:12:42 -07:00
2018-09-21 14:57:12 -04:00
2018-09-21 14:57:12 -04:00
2002-01-05 21:05:47 +00:00
2002-01-05 21:05:47 +00:00
2018-09-21 18:12:42 -07:00
2002-01-05 21:05:47 +00:00
2002-01-05 21:05:47 +00:00
2002-01-05 21:05:47 +00:00
2002-01-05 21:05:47 +00:00
2002-01-05 21:05:47 +00:00
2002-01-05 21:05:47 +00:00
2003-05-11 13:40:01 +00:00
2018-04-25 16:54:50 -04:00
2018-04-25 16:54:50 -04:00
2018-04-25 16:54:50 -04:00
2018-04-25 16:54:50 -04:00
2018-04-25 16:54:50 -04:00
2018-09-21 18:12:42 -07:00
2019-05-09 17:15:14 -07:00
2019-12-03 23:32:12 -05:00
2020-01-13 15:30:23 -05:00
2020-01-25 17:07:45 -08:00
2020-02-10 23:20:58 -05:00
2016-06-19 19:52:28 -04:00
2020-02-12 11:43:25 -08:00
2020-02-12 02:35:35 -08:00
2020-02-11 00:25:27 -05:00
2020-01-01 11:59:43 -05:00
2020-01-27 14:44:29 -05:00
2018-11-11 10:29:52 -05:00
2020-01-14 12:02:10 -05:00
2018-11-11 10:29:52 -05:00
2020-01-14 12:02:26 -05:00
2020-01-19 23:09:53 -05:00
2020-01-20 08:52:59 -05:00
2018-04-25 16:54:50 -04:00
2020-01-14 12:02:57 -05:00
2018-09-20 18:02:48 -04:00
2019-11-14 08:20:38 -05:00
2020-02-08 01:03:25 -05:00
1ec6e6f96b