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.

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

Should be able to adjust spacing/padding of box contents. #1456

Closed
joswarmer opened this issue Jul 28, 2016 · 2 comments
Closed

Should be able to adjust spacing/padding of box contents. #1456

joswarmer opened this issue Jul 28, 2016 · 2 comments
Assignees
@slisson

Comments

@joswarmer
Copy link
Contributor

The content of a box (i.e. a text editor) is very close to the box border. This distance is fixed currently. I would like to be able to specify a "margin" that states the amount of space between the box border and its contents.
@slisson slisson self-assigned this Jul 28, 2016
@slisson slisson mentioned this issue Aug 4, 2016
Closed
19 tasks
@joswarmer joswarmer mentioned this issue Aug 5, 2016
Closed
@joswarmer
Copy link
Contributor Author

There should be separate top, bottom, left and right margins. If there are, #1464 will be resolved as well.

@kbirken kbirken mentioned this issue Aug 6, 2018
Closed
@kbirken
Copy link
Member

kbirken commented Aug 6, 2018

Kamino closed and cloned this issue to JetBrains/MPS-extensions

@kbirken kbirken closed this as completed Aug 6, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@slisson slisson

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@joswarmer @kbirken @slisson