--- /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