HTMLDocument.registerElement is deprecated.

[paolobenve]

Pulsar reports:

Use customElements.define instead of document.registerElement see https://javascript.info/custom-elements

HTMLDocument.registerElement (file:///opt/Pulsar/resources/app.asar/static/index.js:100:12)
registerElement (/home/paolo/.pulsar/packages/symbols-tree-view/node_modules/space-pen/lib/space-pen.js:66:88)
Builder.openTag (/home/paolo/.pulsar/packages/symbols-tree-view/node_modules/space-pen/lib/space-pen.js:297:27)
Builder.tag (/home/paolo/.pulsar/packages/symbols-tree-view/node_modules/space-pen/lib/space-pen.js:274:12)
Function.div (/home/paolo/.pulsar/packages/symbols-tree-view/node_modules/space-pen/lib/space-pen.js:83:49)
Function.content (/home/paolo/.pulsar/packages/symbols-tree-view/lib/symbols-tree-view.coffee:26:19)