diff leim/makefile.w32-in @ 94597:100982f1144d

(--without-makeinfo): New option. If set, absence of suitable makeinfo is not a fatal error.
author Glenn Morris <rgm@gnu.org>
date Sat, 03 May 2008 20:16:15 +0000
parents 107ccd98fa12
children 606f2d163a64 234b6de33fa7
line wrap: on
line diff