diff options
| author | Mike Gerwitz <mtg@gnu.org> | 2018-06-03 00:15:20 -0400 |
|---|---|---|
| committer | Mike Gerwitz <mtg@gnu.org> | 2018-06-03 00:26:45 -0400 |
| commit | e77ebfc973e527c69498e37df4b133c06b9f4d73 (patch) | |
| tree | 8447df2f98c68dc096353a23fdd3bd1c6fa4471f /tools | |
| parent | a4b96ad5639313229583a767e186b9d1bd686b35 (diff) | |
| download | thoughts-e77ebfc973e527c69498e37df4b133c06b9f4d73.tar.gz thoughts-e77ebfc973e527c69498e37df4b133c06b9f4d73.tar.bz2 thoughts-e77ebfc973e527c69498e37df4b133c06b9f4d73.zip | |
:cptt: Add archive
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/texdoc | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/texdoc b/tools/texdoc index 33274dc..1d88212 100755 --- a/tools/texdoc +++ b/tools/texdoc @@ -27,7 +27,9 @@ base="$( basename "$path" )" head -n1 "$main" | sed '1s/^% //;1a\\' ( tr '\n' ' ' \ - | sed 's/\\[^ ]\+\({[^}]\+}\)\?//g;$a\\' + | sed 's/\\[^ ]\+\({[^}]\+}\)\?//g; + s/~/ /g; + $a\\' # all articles should provide PDF and DVI cat <<EOF |