From ec52206bcb149b597dd81913347a36d0ddb6e28b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 11 May 2021 21:12:17 +0200 Subject: for making the docker --- make_docker.sh | 3 +++ 1 file changed, 3 insertions(+) create mode 100755 make_docker.sh (limited to 'make_docker.sh') diff --git a/make_docker.sh b/make_docker.sh new file mode 100755 index 00000000..9665be4d --- /dev/null +++ b/make_docker.sh @@ -0,0 +1,3 @@ +docker build -t compcert_build_env -f compcert_build_env.dockerfile . +docker build -t compcert_kvx -f compcert_kvx.dockerfile . +docker build -t compcert_kvx_pruned -f compcert_kvx_pruned.dockerfile . -- cgit