Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 15
    • Merge requests 15
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !500

Document Makefile flags NO_TEST and MAKE_REF together

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Tej Chajed requested to merge tchajed/iris-coq:document-makefile-options into master Sep 08, 2020
  • Overview 2
  • Commits 1
  • Pipelines 0
  • Changes 2

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).

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: document-makefile-options