diff make-dist @ 3225:1544ad5c9f99

(Info-insert-dir): Ignore duplicate directories.
author Richard M. Stallman <rms@gnu.org>
date Fri, 28 May 1993 23:57:33 +0000
parents 3d245dcabb93
children 27b7aa2bcf21
line wrap: on
line diff