diff make-dist @ 17631:35d8e74c6edb

Use defcustom.
author Richard M. Stallman <rms@gnu.org>
date Sat, 03 May 1997 19:16:43 +0000
parents 892cc20c7d91
children 09cdafe1339f
line wrap: on
line diff