Module Private.Crs_ignoreSource

A .crs-ignore file allows listing files and directories that should be ignored when looking for CRs in the tree.

The primary motivation for this is to help managing files that document the CRs system itself. In these files, we often end up with CRs featured as examples. We don't want to conflate them with actual CRs.

Each line specifies a pattern to ignore, relative to the directory where the ignore file is located. in that directory. The format supports:

  # Lines starting with '#' are comments.
  # Blank lines are ignored.

  # Match specific files by basename
  README.md
  test.ml

  # Shell-style patterns are supported
  *.tmp
  test_*.ml

  # Directories can be ignored (affects all contents recursively)
  _build/**
  node_modules/**