-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathbuild.sh
executable file
·37 lines (29 loc) · 1.17 KB
/
build.sh
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
#!/bin/bash
set -eux
COQ_VER="${1:-8.13.0}"
IMAGE=coq-docset-dash-image:"${COQ_VER//+/-}"
CONTAINER=coq-docset-dash-container-"${COQ_VER//+/-}"
TARGET=build/dash-docset-coq-"${COQ_VER//+/-}"
function die(){
echo "$1"
exit 1
}
cd "$(dirname $(readlink -f "$0"))" || die "cd failed"
docker build -t "$IMAGE" --build-arg COQ_VER="${COQ_VER}" . || die "building docker image failed"
docker create --name "$CONTAINER" "$IMAGE" /bin/sh || die "creating docker container failed"
mkdir -p "$TARGET" || die "mkdir failed"
docker cp "$CONTAINER":/coq/Coq.docset "$TARGET"/ || die "copying from docker container failed"
docker rm "$CONTAINER" || die "deleting docker container failed"
cat <<JSON > "$TARGET/Coq.docset/meta.json" || die "writing to meta.json failed"
{
"name": "Coq",
"revision": "0",
"title": "Coq",
"version": "$COQ_VER"
}
JSON
./tools/edit_info_plist.py "$TARGET/Coq.docset/Contents/Info.plist" || die "editing Info.plist failed"
./tools/remove_absent_link.py "$TARGET/Coq.docset" || die "removing absent link from index failed"
echo "Success: docset saved to $TARGET"
echo "Note: this script does not delete docker image"
echo "execute '$ docker rmi $IMAGE' manually"