Exclude `_opam` directory in `file_check`?
I installed refinedc in a fresh opam local switch and tried refinedc init
, but it says
Directory "/path/to/project/_opam/lib/coq-core/proofs" uses a reserved name.
It works correctly when I ran it in a subdirectory /path/to/project/subdir
.
I think this can be avoided if we add "_opam"
to the ignored_dirs
for file_check
:
https://gitlab.mpi-sws.org/iris/refinedc/-/blob/b41547154b1ae30b75bf76d144a811f699e3b11e/frontend/main.ml#L542