exclude PPs from coverage

This commit is contained in:
Lesenechal Remi 2019-12-11 13:44:47 +01:00
parent 46ac00e94d
commit e8d1e359f4
3 changed files with 3 additions and 0 deletions

View File

@ -1,3 +1,4 @@
[@@@coverage exclude_file]
open Types open Types
open PP_helpers open PP_helpers
open Format open Format

View File

@ -1,3 +1,4 @@
[@@@coverage exclude_file]
open Types open Types
open Format open Format
open PP_helpers open PP_helpers

View File

@ -1,3 +1,4 @@
[@@@coverage exclude_file]
open Simple_utils.PP_helpers open Simple_utils.PP_helpers
open Types open Types
open Format open Format