diff make-dist @ 5108:8c482171bb10

(Man-specified-section-option): New variable. (Man-translate-references): Use that variable.
author Richard M. Stallman <rms@gnu.org>
date Mon, 22 Nov 1993 06:34:22 +0000
parents b4ed97a59663
children 9f18f50000e5
line wrap: on
line diff