diff make-dist @ 58524:92dc214c88ac

Fix the setfilename directive to put the produced file in ../info.
author Eli Zaretskii <eliz@gnu.org>
date Fri, 26 Nov 2004 11:56:50 +0000
parents b5f2181a40b9
children f1e5f5261b95 59dcbfe97385
line wrap: on
line diff