Forked vscode-lean. How do I change "publisher" without error running.

[enjoysmath]

I changed "publisher" in package.json from "jroesch" to "enjoysmath". Here is the error:

I will investigate this today using my debugging skills. However, I'm new to TypeScript.

Thanks.

[bryangingechen]

You may have already figured this out, but this is happening because when you change the publisher, you're effectively creating a separate extension, since VS Code extensions are identified by an id which is publisher.name. Thus, when you launch the Extension Host, both jroesch.lean and enjoysmath.lean are loaded. The error message appears because VS Code can't assign the same command to two extensions.

Possible workarounds:

• disable the jroesch.lean extension while developing enjoysmath.lean
• rename the elements of the commands array in package.json (you will also have to change them where they're referenced in the other parts of the code)

[kim-em]

This can be closed now.