diff options
| author | aiju <devnull@localhost> | 2015-09-28 11:33:06 +0200 |
|---|---|---|
| committer | aiju <devnull@localhost> | 2015-09-28 11:33:06 +0200 |
| commit | 0a3160261d471ec1775024ab1616a9a534626ef3 (patch) | |
| tree | 49faf9e4cc0519030e8e0b3997901867eb6e4e77 /rc | |
| parent | 8a784a3b9b8aa75de59c475acccc68802890f95b (diff) | |
teach doctype how to timepic
Diffstat (limited to 'rc')
| -rwxr-xr-x | rc/bin/doctype | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/rc/bin/doctype b/rc/bin/doctype index 6a2a27d3c..e027fe13b 100755 --- a/rc/bin/doctype +++ b/rc/bin/doctype @@ -23,7 +23,7 @@ ifs=' '{ files=`{echo $*} } -grep -h '\$LIST|\|reference|Jp|^\.(EQ|TS|\[|PS|IS|GS|G1|GD|PP|BM|LP|BP|PI|cstart|begin|TH...)|^\.P$' $* | +grep -h '\$LIST|\|reference|Jp|^\.(EQ|TS|\[|TPS|PS|IS|GS|G1|GD|PP|BM|LP|BP|PI|cstart|begin|TH...)|^\.P$' $* | sort -u | awk ' BEGIN { files = "'$files'" } @@ -33,6 +33,7 @@ BEGIN { files = "'$files'" } /^\.EQ/ { eqn++ } /^\.TS/ { tbl++ } /^\.PS/ { pic++ } +/^\.TPS/ { tpic++; pic++ } /^\.IS/ { ideal++ } /^\.GS/ { tped++ } /^\.G1/ { grap++; pic++ } @@ -55,6 +56,7 @@ END { files = "" } else if (prefer) { x = "cat " files "| '$prefer'| "; files = "" } + if (tpic) { x = x "timepic " files " | "; files = "" } if (tped) { x = x "tped " files " | "; files = "" } if (dag) { x = x "dag " files " | "; files = "" } if (ideal) { x = x "ideal -q " files " | "; files = "" } |