There is not "Developer: Toggle Developer Tools"

[BigFaceBoy]

Is there an existing issue for this?

• I have searched the existing issues

OS/Web Information

• Web Browser: MicroSoft edge
• Local OS: win10
• Remote OS: Centos7
• Remote Architecture: amd64
• code-server --version: v4.96.2

Steps to Reproduce

I can not find "Developer: Toggle Developer Tools" with ctrl+shift+p

Expected

There is "Developer: Toggle Developer Tools"

Actual

There is not "Developer: Toggle Developer Tools"

Logs

Screenshot/Video

No response

Does this bug reproduce in native VS Code?

Yes, this is also broken in native VS Code

Does this bug reproduce in GitHub Codespaces?

Yes, this is also broken in GitHub Codespaces

Are you accessing code-server over a secure context?

• I am using a secure context.

Notes

No response

[code-asher]

I believe this is expected, there is no way to open the dev tools from JavaScript in a browser.

But, you can open them yourself using the browser's menus or keybinding (F12 in my case, might be different depending on the browser, also the keybinding may not work while the terminal is focused since it grabs all the keys).