Mike Gerwitz

Activist for User Freedom

aboutsummaryrefslogtreecommitdiffstats
path: root/tools
diff options
context:
space:
mode:
authorMike Gerwitz <mtg@gnu.org>2018-06-03 00:15:20 -0400
committerMike Gerwitz <mtg@gnu.org>2018-06-03 00:26:45 -0400
commite77ebfc973e527c69498e37df4b133c06b9f4d73 (patch)
tree8447df2f98c68dc096353a23fdd3bd1c6fa4471f /tools
parenta4b96ad5639313229583a767e186b9d1bd686b35 (diff)
downloadthoughts-e77ebfc973e527c69498e37df4b133c06b9f4d73.tar.gz
thoughts-e77ebfc973e527c69498e37df4b133c06b9f4d73.tar.bz2
thoughts-e77ebfc973e527c69498e37df4b133c06b9f4d73.zip
:cptt: Add archive
Diffstat (limited to 'tools')
-rwxr-xr-xtools/texdoc4
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