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

Extraction: reduce krml output unless -d/--debug #3528

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Extraction: reduce krml output unless -d/--debug #3528

wants to merge 2 commits into from

Commits on Oct 6, 2024

  1. Extraction: reduce krml output unless -d/--debug 

    Karamel extraction prints many warnings when definitions cannot be
extracted, but most of these are benign, since they are just types, or
ghost code, etc. This patch disables these warnings unless some
debugging is enabled.
    @mtzguido
    mtzguido committed Oct 6, 2024
    Configuration menu
    Copy the full SHA
    37359a7 View commit details
    Browse the repository at this point in the history

  2. snap

    @mtzguido
    mtzguido committed Oct 6, 2024
    Configuration menu
    Copy the full SHA
    3346ace View commit details
    Browse the repository at this point in the history