# Don't delete these, because they are outside the current directory.
# for file in $(INFO_TARGETS); do rm -f $${file}*; done
# Don't delete these, because they are outside the current directory.
# for file in $(INFO_TARGETS); do rm -f $${file}*; done