private int getIntOption(Options options, String optionName, int defaultValue) {
            String s = options.get(optionName);
            try {
                if (s != null) return Integer.parseInt(s);
            } catch (NumberFormatException e) {
                // silently ignore ill-formed numbers
            }
            return defaultValue;
        }