docker: rename rundocker to run-docker to match previous refactor

README.adoc

@@ -429,7 +429,7 @@ sudo apt-get install docker
 The very first time you launch Docker, create the container with:
 
 ....
-./rundocker setup
+./run-docker setup
 ....
 
 You are now left inside a shell in the Docker guest.
@@ -453,13 +453,13 @@ Ctrl-D
 Restart the container:
 
 ....
-./rundocker
+./run-docker
 ....
 
 In order to use functionality such as <<gdb>>, you need a second shell inside the container. You can either do that with:
 
 ....
-./rundocker sh
+./run-docker sh
 ....
 
 or even better, by starting a <<tmux>> session inside the container. We install `tmux` by default in the container.
@@ -467,12 +467,12 @@ or even better, by starting a <<tmux>> session inside the container. We install
 You can start a second shell and run a command in it at the same time with:
 
 ....
-./rundocker sh ./run-gdb start_kernel
+./run-docker sh ./run-gdb start_kernel
 ....
 
 Docker stops if and only if you quit the initial shell, you can quit this one without consequences.
 
-If you mistakenly run `./rundocker` twice, it opens two mirrored terminals. To quit one of them do link:https://stackoverflow.com/questions/19688314/how-do-you-attach-and-detach-from-dockers-process[]:
+If you mistakenly run `./run-docker` twice, it opens two mirrored terminals. To quit one of them do link:https://stackoverflow.com/questions/19688314/how-do-you-attach-and-detach-from-dockers-process[]:
 
 ....
 Ctrl-P Ctrl-Q
@@ -494,7 +494,7 @@ sudo apt-get install vinagre
 Destroy the docker container:
 
 ....
-./rundocker DELETE
+./run-docker DELETE
 ....
 
 Since we mount the guest's working directory on the host git top-level, you will likely not lose data from doing this, just the `apt-get` installs.
@@ -509,7 +509,7 @@ mv out.host out
 After this, to start using Docker again will you need another:
 
 ....
-./rundocker setup
+./run-docker setup
 ....
 
 Tested on: a760cb1196161e913a94684e03cfeaebf71f0cdd