Github user FlorianHockmann commented on the issue:
https://github.com/apache/tinkerpop/pull/894
Looks like I accidentally added that `Dockerfile`. I should have checked
more carefully what my commit added but shouldn't we prevent that from
happening again with an entry in the `.gitignore` file?---
