The first time this is called, determine what kind of pager to use.
(text, title='')
| 1677 | # --------------------------------------------------------- user interfaces |
| 1678 | |
| 1679 | def pager(text, title=''): |
| 1680 | """The first time this is called, determine what kind of pager to use.""" |
| 1681 | global pager |
| 1682 | pager = get_pager() |
| 1683 | pager(text, title) |
| 1684 | |
| 1685 | def describe(thing): |
| 1686 | """Produce a short description of the given thing.""" |