Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use POSIX-friendly syntax #229

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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 bash)

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