The first time this is called, determine what kind of pager to use.
(text, title='')
| 1631 | # --------------------------------------------------------- user interfaces |
| 1632 | |
| 1633 | def pager(text, title=''): |
| 1634 | """The first time this is called, determine what kind of pager to use.""" |
| 1635 | global pager |
| 1636 | pager = get_pager() |
| 1637 | pager(text, title) |
| 1638 | |
| 1639 | def describe(thing): |
| 1640 | """Produce a short description of the given thing.""" |