+ @for file in $(INFO_DEPS); do \
+ echo "rm -f \"$(DESTDIR)$(infodir)\"/$$file{,-[0-9],.info,.info-[0-9]}"; \
+ rm -f "$(DESTDIR)$(infodir)"/$$file{,-[0-9],.info,.info-[0-9]}; \
+ echo "rm -f \"$(DESTDIR)$(infodir)\"/$$file{,-[0-9],.info,.info-[0-9]}.gz"; \
+ rm -f "$(DESTDIR)$(infodir)"/$$file{,-[0-9],.info,.info-[0-9]}.gz; \
+ done