[doc_tool] Minor GUI improvements
-rw-r--r-- 35149 COPYING
-rw-r--r-- 859 README
drwxr-xr-x - doc
-rw-r--r-- 404 doc_tool.workspace
drwxr-xr-x - management
drwxr-xr-x - packages
drwxr-xr-x - scripts
drwxr-xr-x - src