This patch fixes bug 262. Original implementation doesn't remove empty
directories (created during make install) during make uninstall.
The fix is based on rmdir's -p parameter which removes all empty
directory in the way up.
rmdir --ignore-fail-on-non-empty parameter may not be available on each
platform so that we don't use this parameter and rather use a new
tools/rmdir.sh script which emulates this behavior.
- default value for DEL_DIR updated
- set to tools/rmdir.sh which emulates
rmdir -p --ignore-fail-on-non-empty
- doc_dist_uninstall updated to correctly remove DOC_PATH and
- uninstall-core-dev shouldn't fail when INCLUDE_PATH and LIB_PATH
* tools/rmdir.sh added
- as alreadt mentioned emulates GNU rmdir -p --ignore-fail-on-non-empty
(removes all empty directories in the way up through the given
path, stop with the first non-empty directory and doesn't complain
when the directory is empty. It complains only if given directory
doesn't exist at all)