chiark / gitweb /
Merge branch 'public'
[tripe] / server / make-summary
index 2aff34c6e511f4a5f2a45c64b634bd8e31aa3719..352ebafdd71ba2634b7cc0fe2f63cea8aeda16c7 100755 (executable)
@@ -13,7 +13,7 @@ BEGIN { n = 0; opts = 0; sep = 0; }
 /^\.\\\"\+sep$/ { sep = 1; }
 /^\.\\\"\-sep$/ { sep = 0; }
 /^\.\\\"\-opts$/ { opts = 0; lines[n] = lines[n] ".RE\n"; }
-/^\.SP/ { print; getline; lines[n] = lines[n] $0 "\n"; }
+/^\.SP/ { print ".TP"; getline; lines[n] = lines[n] $0 "\n"; }
 /^\.TP/ { if (opts) { print; getline; lines[n] = lines[n] $0 "\n"; } }
 /^\.SS/ { if (sep) lines[n] = lines[n] ".PP\n"; }