changeset 15010 | 72fbe711e414 |
parent 14997 | aa2aaab41566 |
child 15218 | 39747a9e3c37 |
15009:8c89f588c7aa | 15010:72fbe711e414 |
---|---|
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # Author: Markus Wenzel, TU Muenchen |
4 # Author: Markus Wenzel, TU Muenchen |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6 # |
5 # |
7 # DESCRIPTION: display document (in DVI format) |
6 # DESCRIPTION: display document (in DVI format) |
8 |
7 |
9 |
8 |
10 PRG="$(basename "$0")" |
9 PRG="$(basename "$0")" |