move tools from doc/tools repo to doc repo (doc/tools directory)
check if doc/tools repo is still needed and delete it if not
update repo description in wiki accordingly