Initialiser wieder zurueckgestellt auf JNDI

ulrich

2020-06-25 17727f11c12bd7176af946bb440d509cb558ac22

 web/ui/api.js

@@ -256,6 +256,8 @@
        mode = 'xml';
      } else if(fname.endsWith('properties')) {
        mode = 'xml';
      } else if(fname.endsWith('adoc')) {
        mode = 'text/x-markdown';
      }
      fm_text_edit(resp, mode);
    } else {