Remove the docs submodule
authorBjørn Erik Pedersen <bjorn.erik.pedersen@gmail.com>
Mon, 26 Jun 2017 18:39:53 +0000 (20:39 +0200)
committerBjørn Erik Pedersen <bjorn.erik.pedersen@gmail.com>
Mon, 26 Jun 2017 18:45:04 +0000 (20:45 +0200)
commit31393f6024416ea1b2e61d1080dfd7104df36eda
tree080dd84a7ee80ae6a65f6a540af3e44ad8040e23
parentaff1ac3235b6c075d01f7237addf44fecdd36d82
Remove the docs submodule

Will be replaced by a Git subtree.

See #3647
.gitmodules
docs [deleted submodule]