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

Don't build with -warn-error +A for releases #38

Merged
merged 2 commits into from
Nov 11, 2023
Merged

Don't build with -warn-error +A for releases #38

merged 2 commits into from
Nov 11, 2023

Commits on Nov 9, 2023

  1. Remove toplevel/Makefile 

    It's no longer required (and broken) since PR#29.
    @dra27
    dra27 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    4d1fc81 View commit details
    Browse the repository at this point in the history

  2. Build with -warn-error +A only in the dev profile 

    Use Dune's env stanza to apply -warn-error +A only in the (default) dev
profile.

The Makefile now recognises an equivalent PROFILE variable which should
be either be auto, dev, or release. If the build tree includes a .git
directory then the dev profile is assumed.

CI explicitly specifies PROFILE=dev and the opam installation explicitly
specifies PROFILE=release.
    @dra27
    dra27 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    2bcc488 View commit details
    Browse the repository at this point in the history