* Richard W.M. Jones: >> EXTRA_DIST = \ >> - $(SOURCES) >> + $(filter-out config.ml.in,$(SOURCES)) > > I think you mean config.ml here? config.ml.in is needed by > ./configure AFAICT. Of course. Thanks. -Hilko