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.

Sign up for GitHub

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

Jump to bottom

Add print_margin and filename option to Ace widget #1391

Merged

philippjfr merged 3 commits into master from ace_print_margin

Jun 12, 2020

Member

philippjfr commented Jun 9, 2020 •

edited

Loading

The print margin often overlaps with other components so this PR allows disabling it.

Update docs
Fixes Determine language for Ace editor from file extension #1404

philippjfr added 2 commits

June 9, 2020 15:50


          Add print_margin option to Ace widget

685131b


          Add filename option to Ace widget

1d5988c

philippjfr changed the title ~~Add print_margin option to Ace widget~~ Add print_margin and filename option to Ace widget


          Fixed Ace.language default

926c149

philippjfr merged commit 914d534 into master

philippjfr deleted the ace_print_margin branch

June 12, 2020 12:56

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet