File tree Expand file tree Collapse file tree 3 files changed +5
-17
lines changed
src/lib/mina_version/normal Expand file tree Collapse file tree 3 files changed +5
-17
lines changed Original file line number Diff line number Diff line change 354354 PLONK_WASM_WEB = "${ pkgs . plonk_wasm } /web" ;
355355
356356 configurePhase = ''
357- export MINA_ROOT="$PWD"
358357 export -f patchShebangs isScript
359358 fd . --type executable -x bash -c "patchShebangs {}"
360359 export -n patchShebangs isScript
Original file line number Diff line number Diff line change 99 (implements mina_version))
1010
1111(rule
12- (targets mina_version.ml)
13- (deps
14- (sandbox none)
15- (:< gen.sh)
16- (universe))
17- (action
18- (run bash %{<} %{targets})))
12+ (target mina_version.ml)
13+ (deps (:< gen.sh))
14+ (action (run %{<} %{target})))
Original file line number Diff line number Diff line change 11#! /usr/bin/env bash
22set -euo pipefail
33
4- # we are nested 6 directories deep (_build/<context>/src/lib/mina_version/normal)
5- if [ -z ${MINA_COMMIT_SHA1+x} ]; then
6- root=" ${MINA_ROOT-$(git rev-parse --show-toplevel || echo ../ ../ ../ ../ ../ ..)} "
7- pushd " $root " > /dev/null
8- id=" ${MINA_COMMIT_SHA1-$(git rev-parse --verify HEAD || echo " <unknown>" )} "
9- popd > /dev/null
10- else
11- id=" ${MINA_COMMIT_SHA1} "
12- fi
4+ target=$1
135
6+ id=" ${MINA_COMMIT_SHA1:- $(git rev-parse --verify HEAD 2>/ dev/ null || echo " <unknown>" )} "
147id_short=" $( printf " %s" " $id " | cut -c1-8) "
158
169{
You can’t perform that action at this time.
0 commit comments