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