Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feature request: Change default values for widget mode #327

Open
iulian-birlica opened this issue Jan 22, 2023 · 0 comments
Open

Feature request: Change default values for widget mode #327

iulian-birlica opened this issue Jan 22, 2023 · 0 comments

Comments

@iulian-birlica
Copy link

Hello! I have been playing around with the vscode-lean extension, and I find the widget-mode "Props only" option to be an excellent didactic tool, keeping attention on the important things during a presentation.

The only problem that I encountered is that I have to manually click "Props only" for every line (or statement change), making it cumbersome to use.

I am not sure this is a proper feature request, because this feature may already exist, but I searched the documentation, github issues, and the internet, and I could not find something to set default values in widget-mode (Zulip chat seems hard to search for some reason, returning results for every "Props" word in discussions).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant