Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
driver.mld: Fix Mdx error hidden by Dune error
As the driver reports errors with promotion and not with an exit status, the driver could fail to generate `driver-benchmarks.json`, in which case Dune would complain about the missing target and would not show the diff containing the error.
- Loading branch information