Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: mirage/mirage
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: ed630b584216
Choose a base ref
...
head repository: mirage/mirage
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: af85b6593cb6
Choose a head ref
  • 2 commits
  • 1 file changed
  • 2 contributors

Commits on Mar 20, 2016

  1. Remove warn_error from default tags

    Adding warn_error to the default tags for warnings that have been
    enabled in the same step is a regression, since there has been no
    inermediate period where this warnings could have been fixed.  This
    change removes the warn_error tag from the default tags.
    
    Fixes: #520
    ansiwen committed Mar 20, 2016
    Copy the full SHA
    d0cbe2b View commit details
  2. Merge pull request #521 from ansiwen/no_warn_error

    Remove warn_error from default tags
    samoht committed Mar 20, 2016

    Verified

    This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
    Copy the full SHA
    af85b65 View commit details
Showing with 1 addition and 1 deletion.
  1. +1 −1 lib/mirage.ml
2 changes: 1 addition & 1 deletion lib/mirage.ml
Original file line number Diff line number Diff line change
@@ -1294,7 +1294,7 @@ let configure_makefile ~target ~root ~name info =
append fmt "LIBS = %s" libraries;
append fmt "PKGS = %s" packages;
let default_tags =
"warn_error(+1..49),warn(A-4-41-44),debug,bin_annot,\
"warn(A-4-41-44),debug,bin_annot,\
strict_sequence,principal,safe_string"
in
begin match target with