void (Element element) { if (myRedirectInput) { JDOMExternalizerUtil.writeField(element, REDIRECT_INPUT, "true"); } if (myInputFile != null) { JDOMExternalizerUtil.writeField(element, INPUT_FILE, myInputFile); } }