diff options
| author | Alasdair | 2019-02-08 23:06:47 +0000 |
|---|---|---|
| committer | Alasdair | 2019-02-08 23:12:18 +0000 |
| commit | ee2eb2bad10ad8d7c730538f239474ce103efa16 (patch) | |
| tree | 57e1fe86d568c855609c623b8c414a9cc0c14693 /src/bytecode_util.ml | |
| parent | ee7a00b1ede8ed991d5fac416f93b09b9a5b0d01 (diff) | |
Cleanup src Makefile
When we are building from git, we put the git version info in manifest.ml, so
we'll get the following from sail -v
Sail $last_git_tag ($branch @ $commit_sha)
If we are be built from opam we can't assume we are in a git repository as
opam downloads specific tags as tarballs, so instead we check for the precense
of SHARE_DIR which is set by our opam build script, and instead output
Sail 0.8 (sail2 @ opam)
which is the next git tag (current is 0.7.1, this must be updated by hand),
the branch name from which opam releases are generated and then opam rather
than the commit SHA.
I also removed the Makefile-non-opam file as it's bitrotted and unused
Diffstat (limited to 'src/bytecode_util.ml')
0 files changed, 0 insertions, 0 deletions
