Skip to content

Document Makefile flags NO_TEST and MAKE_REF together

Tej Chajed requested to merge tchajed/iris-coq:document-makefile-options into master

Alternate proposal to !466 (closed) that puts the documentation a little deeper so it's read by developers and not users.

I decided to mention the flags in both the Makefile.coq.local and CONTRIBUTING.md. I'm open to dropping one of these (but not both).

Merge request reports