aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--compcert_build_env.dockerfile (renamed from Dockerfile.build_env)0
-rw-r--r--compcert_kvx.dockerfile (renamed from Dockerfile)0
-rw-r--r--compcert_kvx_pruned.dockerfile (renamed from Dockerfile.prune)0
-rwxr-xr-xmake_docker.sh3
4 files changed, 3 insertions, 0 deletions
diff --git a/Dockerfile.build_env b/compcert_build_env.dockerfile
index de339e55..de339e55 100644
--- a/Dockerfile.build_env
+++ b/compcert_build_env.dockerfile
diff --git a/Dockerfile b/compcert_kvx.dockerfile
index 21b15308..21b15308 100644
--- a/Dockerfile
+++ b/compcert_kvx.dockerfile
diff --git a/Dockerfile.prune b/compcert_kvx_pruned.dockerfile
index c122cb83..c122cb83 100644
--- a/Dockerfile.prune
+++ b/compcert_kvx_pruned.dockerfile
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 .