'make distclean' deletes too many files

[Bruno Haible]

Given a tarball, the sequence of commands

  $ ./configure
  $ make
  $ make clean
  $ make distclean

should not leave any files around, and should not remove files that were in
the tarball.

In the current state, the following files are deleted although they shouldn't:

  doc/pvm-insns.texi
  jitter/bin/jitter-config.1
  jitter/example-vms/jitterlisp/jitterlispvm-vm.h
  jitter/example-vms/jitterlisp/jitterlispvm-vm1.c
  jitter/example-vms/jitterlisp/jitterlispvm-vm2.c
  jitter/example-vms/uninspired/uninspired-vm-main.c
  jitter/example-vms/uninspired/uninspired-vm.h
  jitter/example-vms/uninspired/uninspired-vm1.c
  jitter/example-vms/uninspired/uninspired-vm2.c
  jitter/jitterc/jitter.1

Here's a patch to fix the first among these. I leave the rest to Luca.

doc/pvm-insns.texi is in the tarball. Why? Not because it needs special tools
to build ('egrep' is a bit unportable, but not _that_ much). But really because
if we omitted it from the tarball, the Makefile rules for poke.info and
poke.text would attempt to recreate it even though poke.info and poke.text are
in the tarball.

0001-Fix-make-distclean-to-not-remove-doc-pvm-insns.texi.patch
Description: Text Data