-
Notifications
You must be signed in to change notification settings - Fork 68
Expand file tree
/
Copy pathrun
More file actions
executable file
·65 lines (55 loc) · 1.81 KB
/
Copy pathrun
File metadata and controls
executable file
·65 lines (55 loc) · 1.81 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
#!/usr/bin/env bash
set -euo pipefail
DIST_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
CALLER_MATHCODE_WEBUI_PORT_SET="${MATHCODE_WEBUI_PORT+x}"
CALLER_MATHCODE_WEBUI_PORT="${MATHCODE_WEBUI_PORT-}"
CALLER_MATHCODE_WEBUI_WORKSPACE_SET="${MATHCODE_WEBUI_WORKSPACE+x}"
CALLER_MATHCODE_WEBUI_WORKSPACE="${MATHCODE_WEBUI_WORKSPACE-}"
if [[ -f "$DIST_DIR/.env" ]]; then
set -a
source "$DIST_DIR/.env"
set +a
fi
is_executable_file() {
[[ -f "$1" && -x "$1" ]]
}
local_elan_tool_path() {
local tool="$1"
local elan_bin="$DIST_DIR/.local/elan/bin"
if is_executable_file "$elan_bin/$tool"; then
printf '%s\n' "$elan_bin/$tool"
return 0
fi
if is_executable_file "$elan_bin/$tool.exe"; then
printf '%s\n' "$elan_bin/$tool.exe"
return 0
fi
return 1
}
if local_elan_tool_path lean >/dev/null && local_elan_tool_path lake >/dev/null; then
unset ELAN_TOOLCHAIN
export ELAN_HOME="$DIST_DIR/.local/elan"
export PATH="$DIST_DIR/.local/elan/bin:$PATH"
fi
export MATHCODE_RELEASE_ROOT="$DIST_DIR"
export LEAN_PROJECT_DIR="${LEAN_PROJECT_DIR:-$DIST_DIR/lean-workspace}"
if [[ "${1:-}" == "webui" || "${1:-}" == "--webui" ]]; then
shift
if [[ ! -x "$DIST_DIR/mathcode-webui" ]]; then
printf 'MathCode WebUI binary is not installed here yet. Run `bash setup.sh` first.\n' >&2
exit 1
fi
if [[ "$CALLER_MATHCODE_WEBUI_PORT_SET" == "x" ]]; then
export MATHCODE_WEBUI_PORT="$CALLER_MATHCODE_WEBUI_PORT"
fi
if [[ "$CALLER_MATHCODE_WEBUI_WORKSPACE_SET" == "x" ]]; then
export MATHCODE_WEBUI_WORKSPACE="$CALLER_MATHCODE_WEBUI_WORKSPACE"
fi
export MATHCODE_WEBUI_ENV_LOADED=1
exec "$DIST_DIR/mathcode-webui" "$@"
fi
if [[ ! -x "$DIST_DIR/mathcode" ]]; then
printf 'MathCode binary is not installed here yet. Run `bash setup.sh` first.\n' >&2
exit 1
fi
exec "$DIST_DIR/mathcode" "$@"