search

herd / herdtools7

The Herd toolsuite to deal with .cat memory models (version 7.xx)
Other
220 stars 57 forks source link

[action] Use dev profile for CI #942

Closed maranget closed 1 month ago

maranget commented 1 month ago

Using our "dev" profile will trigger some error whenever our "release" flags a warning. As a result, warnings will not reach production code...

HadrienRenaud commented 1 month ago

I'm curious @maranget, how did you choose such list of warnings?

maranget commented 1 month ago

I'm curious @maranget, how did you choose such list of warnings?

I do not remember, I have been using this list for ages. Perhaps it is time to review it?