mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
WEB-6302 fix migrating from obsolete buggy setting html5 language level to the new one
This commit is contained in:
@@ -381,7 +381,7 @@ public class ExternalResourceManagerImpl extends ExternalResourceManagerEx imple
|
||||
Element child = element.getChild(HTML_DEFAULT_DOCTYPE_ELEMENT);
|
||||
if (child != null) {
|
||||
String text = child.getText();
|
||||
if (FileUtil.toSystemIndependentName(text).endsWith("idea.jar!/resources/html5-schema/html5.rnc")) {
|
||||
if (FileUtil.toSystemIndependentName(text).endsWith(".jar!/resources/html5-schema/html5.rnc")) {
|
||||
text = HTML5_DOCTYPE_ELEMENT;
|
||||
}
|
||||
myDefaultHtmlDoctype = text;
|
||||
|
||||
Reference in New Issue
Block a user