# HG changeset patch
# User Edouard Tisserant <edouard.tisserant@gmail.com>
# Date 1513441702 -3600
# Node ID 12390414aed0705d1ec03129d9f1442a5f197cd9
# Parent  bec145483ea8463947fd5ba942623a765b7df633
added helper scripts to use docker build

diff -r bec145483ea8 -r 12390414aed0 enter_docker.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/enter_docker.sh	Sat Dec 16 17:28:22 2017 +0100
@@ -0,0 +1,7 @@
+#!/bin/bash
+
+# this script is given as an exemple
+# I use it to have a shell running in ready-to-build container
+# obtained with rebuild_docker.sh
+
+docker start -i current
diff -r bec145483ea8 -r 12390414aed0 rebuild_docker.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/rebuild_docker.sh	Sat Dec 16 17:28:22 2017 +0100
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+# this script is given as an exemple
+# I use it to prepare a ready-to-build container
+# and then use that container with enter_docker.sh
+
+docker rm current
+docker rmi beremiz_builder
+docker build --build-arg UID=$(id -u) --build-arg GID=$(id -g) -t beremiz_builder .
+docker create \
+       --name current \
+       -v ~/src:/home/devel/src \
+       -v ~/build/:/home/devel/build \
+       -v ~/.bash_history:/home/devel/.bash_history \
+       -w /home/devel/build \
+       -i -t beremiz_builder /bin/bash