diff options
| author | Robert Norton | 2018-04-26 15:12:24 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-04-26 15:12:24 +0100 |
| commit | 0ee8e4d2dd1958d9a1aa45fbe8f67861d18e548c (patch) | |
| tree | 63d51b0a53508c7a79a32e1f667a28a4250ec4bb /src/lem_interp/run_interp.ml | |
| parent | ae12f0feb0978eb1f511482293b1d1a20fb04ee4 (diff) | |
Add a new SHARE_DIR argument to use when doing opam build. For non-opam builds this defaults to git root.
Diffstat (limited to 'src/lem_interp/run_interp.ml')
0 files changed, 0 insertions, 0 deletions