[PPL-devel] make ; make distclean is not idempotent

[Michael Tautschnig]

Hi all,

It seems that make distclean still removes stuff (or fails to do so) that is
part of your .tar.gz distribution. This is the output after a cancelled build,
running make distclean afterwards, and then restarting:

This one (and possibly other non-empty ones) did not get removed by make distclean:
dpkg-source: warning: newly created empty file 'tests/Box/dirty_marker' will not be represented in diff

These are part of the .tar.gz, but have been removed by make distclean:
dpkg-source: warning: ignoring deletion of file Watchdog/doc/devref.doxyconf-html
dpkg-source: warning: ignoring deletion of file Watchdog/doc/user.doxyconf-latex
dpkg-source: warning: ignoring deletion of file Watchdog/doc/devref.doxyconf-latex
dpkg-source: warning: ignoring deletion of file Watchdog/doc/user.doxyconf-html
dpkg-source: warning: ignoring deletion of file doc/devref.doxyconf-html
dpkg-source: warning: ignoring deletion of file doc/devref-language-interface.doxyconf
dpkg-source: warning: ignoring deletion of file doc/user.doxyconf-latex
dpkg-source: warning: ignoring deletion of file doc/devref.doxyconf-latex
dpkg-source: warning: ignoring deletion of file doc/user.doxyconf-html
dpkg-source: warning: ignoring deletion of file doc/user-language-interface.doxyconf
dpkg-source: warning: ignoring deletion of file src/ppl-config.cc

I don't consider this really critical, but I would be nice if future versions of
ppl could handle this properly.

Best,
Michael