Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This avoids fed-gen race condition. It will lead to quadratically many file writes in CI. It also allows users to put their own files in the include directory if they like. I am not sure if this is a "feature" that we actually want. We can discuss later.
- Loading branch information