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

Add benchcomp filter command #3105

Merged
merged 3 commits into from
Mar 26, 2024
Merged

Add benchcomp filter command #3105

merged 3 commits into from
Mar 26, 2024

Commits on Mar 25, 2024

  1. Add benchcomp filter command 

    This allows benchcomp to pass the list of results to an external program
for modification before the results are visualized. This can be used,
for example, to visualize only a relevant subset of results.
    @karkhaz
    karkhaz committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    8260439 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into kk-benchcomp-filter

    @karkhaz
    karkhaz authored Mar 25, 2024
    Configuration menu
    Copy the full SHA
    0d8bcd3 View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2024

  1. Clarify that filter scripts can emit JSON

    @karkhaz
    karkhaz committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    4da7143 View commit details
    Browse the repository at this point in the history