@echo "************************************************************"
@echo "configure changed! You should probably reconfigure manually."
@echo "************************************************************"
@echo "************************************************************"
@echo "configure changed! You should probably reconfigure manually."
@echo "************************************************************"