Problems about OPTIONS menu in Makefile fixed. How-To-Repeat: updating port files
State Changed From-To: open->closed Committed, thanks! Note: I've fixed default behaviour when builds with BATCH=1