diff --git a/doc/tools.html b/doc/tools.html index 86bedd1dc..907abe68b 100644 --- a/doc/tools.html +++ b/doc/tools.html @@ -13,10 +13,10 @@