diff --git a/doc/tools/gitwash b/doc/tools/gitwash deleted file mode 160000 index e02c2af7..00000000 --- a/doc/tools/gitwash +++ /dev/null @@ -1 +0,0 @@ -Subproject commit e02c2af711ff6b905a3e75f99f55e078a88e6b7e