Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[menhir] Call menhir from root scope directory as to improve error re…
…porting. This is a common problem in a few Dune tools: if a menhir file is inside a sub-directory, the tool will be invoked from the subdir, however the Dune call was likely from the top-level directory and the error/warning messages won't be correct. I am not sure this is the right way to address this problem, in particular what will happen if Dune is called from some parallel sub-directory. Suggestions welcome. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
- Loading branch information