This likely became stale
tree434199d9d9be21ba1d401610b39dd38156422644
-rw-r--r-- 53 .dir-locals.el
-rw-r--r-- 50 .gitignore
-rw-r--r-- 221 .mailmap
-rw-r--r-- 12 .merlin
-rw-r--r-- 32 .ocp-indent
-rw-r--r-- 759 BUILDING
-rw-r--r-- 50 INSTALL
-rw-r--r-- 7599 KEYS
-rw-r--r-- 196 LICENSE
-rw-r--r-- 271 README
-rw-r--r-- 806 Thanks
drwxr-xr-x - adoc
-rwxr-xr-x 10117 build.bash
-rw-r--r-- 49783 config.ml
-rw-r--r-- 1734 cutils.c
-rw-r--r-- 753 cutils.h
-rw-r--r-- 3498 genconfstr.sh
-rw-r--r-- 11843 glfont.c
-rw-r--r-- 1855 glutils.ml
-rw-r--r-- 969 helputils.ml
-rw-r--r-- 176 keys.ml
drwxr-xr-x - lablGL
-rw-r--r-- 115067 link.c
-rw-r--r-- 22641 listview.ml
-rw-r--r-- 154796 main.ml
drwxr-xr-x - misc
-rw-r--r-- 9197 parser.ml
-rw-r--r-- 2831 todo.org
-rw-r--r-- 123 unisyms.ml
-rw-r--r-- 9335 utils.ml
-rw-r--r-- 1593 wsi.mli
drwxr-xr-x - wsi