Skip to content

Commit

Permalink
Use POSIX syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
concatime committed Feb 14, 2022
1 parent 7e02ba7 commit d8c0db9
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 7 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ test: all

# Auto-detection
pre:
@which fstar.exe >/dev/null 2>&1 || [ -x $(FSTAR_HOME)/bin/fstar.exe ] || \
@command -v fstar.exe >/dev/null 2>&1 || [ -x $(FSTAR_HOME)/bin/fstar.exe ] || \
{ echo "Didn't find fstar.exe in the path or in FSTAR_HOME (which is: $(FSTAR_HOME))"; exit 1; }
@ocamlfind query fstarlib >/dev/null 2>&1 || [ -f $(FSTAR_HOME)/bin/fstarlib/fstarlib.cmxa ] || \
{ echo "Didn't find fstarlib via ocamlfind or in FSTAR_HOME (which is: $(FSTAR_HOME)); run $(MAKE) -C $(FSTAR_HOME)/ulib/ml"; exit 1; }
Expand Down
8 changes: 4 additions & 4 deletions build_local.sh
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
#!/usr/bin/env bash
#!/bin/sh
set -e

# Look for config.json file
FILE=".docker/build/config.json"
if [[ ! -f $FILE ]]; then
if [ ! -f $FILE ]; then
echo "File $FILE does not exist."
fi

# In case you want to build windows, change agentOS here to windows-nt if OSTYPE is not working
agentOS=linux
if [[ "$OSTYPE" == "cygwin" ]]; then
if [ "$OSTYPE" == "cygwin" ]; then
agentOS=linux #windows-nt
fi

Expand All @@ -32,7 +32,7 @@ REQUESTEDBRANCHNAME=$(jq -c -r ".BranchName" "$FILE")
REQUESTEDCOMMITID=$(jq -c -r ".BaseContainerImageTagOrCommitId" "$FILE")
COMMITURL=$(jq -c -r ".GithubCommitUrl" "$FILE")/$REQUESTEDBRANCHNAME

if [[ $(jq -c -r ".BaseContainerImageTagOrCommitId" "$FILE") -ne "latest" ]]; then
if [ "$(jq -c -r '.BaseContainerImageTagOrCommitId' "$FILE")" -ne "latest" ]; then
COMMITURL=$(jq -c -r ".GithubCommitUrl" "$FILE")/$REQUESTEDCOMMITID
fi

Expand Down
2 changes: 1 addition & 1 deletion kremlib/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ ROOTS = $(wildcard *.fst) $(wildcard *.fsti) $(wildcard ../runtime/*.fst) \
clean: clean-c
rm -rf *.checked *.source .depend

SHELL:=$(shell which bash)
SHELL:=$(shell command -v sh || echo /bin/sh)

clean-c:
rm -rf dist out extract-all */*.o
Expand Down
2 changes: 1 addition & 1 deletion src/Driver.ml
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,7 @@ let detect_fstar () =
fstar_home := r;
fstar := r ^^ "bin" ^^ "fstar.exe"
with Not_found -> try
fstar := read_one_line "which" [| "fstar.exe" |];
fstar := read_one_line "sh" [| "-c"; "command -v fstar.exe" |];
fstar_home := d (d !fstar);
if not !Options.silent then
KPrint.bprintf "FSTAR_HOME is %s (via fstar.exe in PATH)\n" !fstar_home
Expand Down

0 comments on commit d8c0db9

Please sign in to comment.