disable warning 60 with --dev

This commit is contained in:
hhugo 2017-05-14 13:06:22 +01:00 committed by GitHub
parent 15f43615c5
commit c880cd3e2d
1 changed files with 1 additions and 0 deletions

View File

@ -17,6 +17,7 @@ let dev_mode_warnings =
; 48
; 58
; 59
; 60
])
let default_flags () =