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

Jump to bottom

indention after 'package ... endpackage' is one level too deep #1048

Closed
veripoolbot opened this issue Mar 17, 2016 · 3 comments
Closed

indention after 'package ... endpackage' is one level too deep #1048

veripoolbot opened this issue Mar 17, 2016 · 3 comments
Labels
indents

Comments

@veripoolbot
Copy link
Collaborator

Author Name: Alex Reed
Original Redmine Issue: 1048 from https://www.veripool.org

 ...
endpackage
  // this should indent to left margin, but indents one stop to right
@veripoolbot
Copy link
Collaborator Author

Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2017-11-19T13:32:51Z

Still a problem, perhaps someone would like to contribute a patch?

@gmlarumbe
Copy link
Contributor

Seems that #1765 also fixed this issue. The following snippet gets indented correctly from 252bff3:

package
    // ...
endpackage
// this should indent to left margin, but indents one stop to right

@wsnyder
Copy link
Member

wsnyder commented May 16, 2022

Great!

@wsnyder wsnyder closed this as completed May 16, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
indents
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@wsnyder @gmlarumbe @veripoolbot