Skip to content

Commit

Permalink
fixup! prepare for trmc
Browse files Browse the repository at this point in the history
  • Loading branch information
gasche committed Jul 23, 2020
1 parent f60b771 commit 7584935
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions utils/warnings.ml
Expand Up @@ -389,8 +389,7 @@ let parse_opt errors active errflag s =
loop (i+1)
| _ -> error ()
in
loop 0;
errors.(69) <- false (* Missed potential TRMC call is not an error *)
loop 0
;;

let parse_options errflag s =
Expand Down

0 comments on commit 7584935

Please sign in to comment.