File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -51,7 +51,7 @@ test: all
5151
5252# Auto-detection
5353pre :
54- @which fstar.exe > /dev/null 2>&1 || [ -x $( FSTAR_HOME) /bin/fstar.exe ] || \
54+ @command -v fstar.exe > /dev/null 2>&1 || [ -x $( FSTAR_HOME) /bin/fstar.exe ] || \
5555 { echo " Didn't find fstar.exe in the path or in FSTAR_HOME (which is: $( FSTAR_HOME) )" ; exit 1; }
5656 @ocamlfind query fstarlib > /dev/null 2>&1 || [ -f $( FSTAR_HOME) /bin/fstarlib/fstarlib.cmxa ] || \
5757 { echo " Didn't find fstarlib via ocamlfind or in FSTAR_HOME (which is: $( FSTAR_HOME) ); run $( MAKE) -C $( FSTAR_HOME) /ulib/ml" ; exit 1; }
Original file line number Diff line number Diff line change 1- #! /usr/ bin/env bash
1+ #! /bin/sh
22set -e
33
44# Look for config.json file
55FILE=" .docker/build/config.json"
6- if [[ ! -f $FILE ] ]; then
6+ if [ ! -f $FILE ]; then
77 echo " File $FILE does not exist."
88fi
99
1010# In case you want to build windows, change agentOS here to windows-nt if OSTYPE is not working
1111agentOS=linux
12- if [[ " $OSTYPE " == " cygwin" ] ]; then
12+ if [ " $OSTYPE " == " cygwin" ]; then
1313 agentOS=linux # windows-nt
1414fi
1515
@@ -32,7 +32,7 @@ REQUESTEDBRANCHNAME=$(jq -c -r ".BranchName" "$FILE")
3232REQUESTEDCOMMITID=$( jq -c -r " .BaseContainerImageTagOrCommitId" " $FILE " )
3333COMMITURL=$( jq -c -r " .GithubCommitUrl" " $FILE " ) /$REQUESTEDBRANCHNAME
3434
35- if [[ $( jq -c -r " .BaseContainerImageTagOrCommitId" " $FILE " ) -ne " latest" ] ]; then
35+ if [ " $( jq -c -r ' .BaseContainerImageTagOrCommitId' " $FILE " ) " -ne " latest" ]; then
3636 COMMITURL=$( jq -c -r " .GithubCommitUrl" " $FILE " ) /$REQUESTEDCOMMITID
3737fi
3838
Original file line number Diff line number Diff line change @@ -47,7 +47,7 @@ ROOTS = $(wildcard *.fst) $(wildcard *.fsti) $(wildcard ../runtime/*.fst) \
4747clean : clean-c
4848 rm -rf * .checked * .source .depend
4949
50- SHELL: =$(shell which bash)
50+ SHELL: =$(shell command -v bash)
5151
5252clean-c :
5353 rm -rf dist out extract-all * /* .o
Original file line number Diff line number Diff line change @@ -221,7 +221,7 @@ let detect_fstar () =
221221 fstar_home := r;
222222 fstar := r ^^ " bin" ^^ " fstar.exe"
223223 with Not_found -> try
224- fstar := read_one_line " which " [| " fstar.exe" |];
224+ fstar := read_one_line " sh " [| " -c " ; " command -v fstar.exe" |];
225225 fstar_home := d (d ! fstar);
226226 if not ! Options. silent then
227227 KPrint. bprintf " FSTAR_HOME is %s (via fstar.exe in PATH)\n " ! fstar_home
You can’t perform that action at this time.
0 commit comments