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

TableGenerator: Columns sorted alphabetically? #259

Closed
kfriedberger opened this issue Oct 4, 2017 · 0 comments
Closed

TableGenerator: Columns sorted alphabetically? #259

kfriedberger opened this issue Oct 4, 2017 · 0 comments
Labels
enhancement

Comments

@kfriedberger
Copy link
Member

kfriedberger commented Oct 4, 2017 •
edited
Loading

Since the last release, columns in html-tables are sorted alphabetically. As the column status is special (colorful and bold), I would like it to be at first position again, not sorted into the middle between cputime and walltime.
If we plan to have more columns with name status, e.g. for multi-property-verification, perhaps put all of them to the front of the alphabet.
@kfriedberger kfriedberger changed the title TbleGenerator: Columns sorted alphabetically? TableGenerator: Columns sorted alphabetically? Oct 4, 2017
@kfriedberger kfriedberger mentioned this issue Oct 4, 2017
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement
Milestone
No milestone
Development

No branches or pull requests
1 participant
@kfriedberger