Fix broken gwiad_plugin_distrib
tree9b6d0da51c24872e5d758f8f6f4b3b725ba5344b
-rw-r--r-- 201 .gitignore
-rw-r--r-- 17987 COPYING
-rw-r--r-- 1640 analyse.sh
drwxr-xr-x - config
-rw-r--r-- 616 diouzhtu.check
drwxr-xr-x - diouzhtu
drwxr-xr-x - diouzhtu2html
drwxr-xr-x - external_libraries
drwxr-xr-x - gwiad_wiki_service
-rw-r--r-- 6572 makefile
-rw-r--r-- 1820 mk.config
-rwxr-xr-x 3736 shared.gpr