aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/make_git_revision.sh
AgeCommit message (Collapse)Author
2018-10-03[dune] [opam] Install `revision` file when building with Dune.Emilio Jesus Gallego Arias
Fixes #8621