Re: 'make distclean' deletes too many files

[Bruno Haible]

> >   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.
> 
> Makes sense.
> OK for master.

Pushed it (the part that fixes doc/).