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