patched_dtd => patch_dtd

diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index 8ad40ce64ceaa580520e4dd13919c9a28aa1179c..9e1fe8982fcc87e4a92fd79e9e72f86f3a0f3fc7 100644 (file)
--- a/helm/on-line/javascript/control.js
+++ b/helm/on-line/javascript/control.js
@@ -123,7 +123,7 @@ function makeURL(type,uri,cicflags,typesflags)
     if (format == "types") ext = ".types"
     else if (format == "ann") ext = ".ann";
     url = getterURL + "getxml?uri=" + uri + ext + "&format=" + mode_list[5] +
-     "&patched_dtd=" + mode_list[6];
+     "&patch_dtd=" + mode_list[6];
   } else {
     if (format == "html" && type == "cic") {
       keys = "C1,HC2,L&param.processorURL=" + escape(processorURL) +