Fix for botched merge of options.h