Avoid doing work in a pipe
tree5a14a46bb8dd3b428b2db952a8ab6d724f94a904
-rw-r--r-- 58 .dir-locals.el
drwxr-xr-x - .github
-rw-r--r-- 50 .gitignore
-rw-r--r-- 238 .mailmap
-rw-r--r-- 12 .merlin
-rw-r--r-- 32 .ocp-indent
-rw-r--r-- 913 BUILDING
-rw-r--r-- 50 INSTALL
-rw-r--r-- 192 LICENSE
-rw-r--r-- 271 README
-rw-r--r-- 806 Thanks
drwxr-xr-x - adoc
-rwxr-xr-x 112 ahbs
-rwxr-xr-x 9838 build.bash
-rw-r--r-- 47087 config.ml
-rw-r--r-- 1464 cutils.c
-rw-r--r-- 741 cutils.h
-rw-r--r-- 474 diag.h
-rw-r--r-- 3189 ffi.ml
-rw-r--r-- 3464 genconfstruct.sh
-rw-r--r-- 11357 glfont.c
-rw-r--r-- 1073 glutils.ml
-rw-r--r-- 7716 help.ml
-rw-r--r-- 168 help.mli
-rw-r--r-- 614 keys.ml
drwxr-xr-x - lablGL
-rw-r--r-- 99160 link.c
-rw-r--r-- 144412 main.ml
-rw-r--r-- 0 main.mli
drwxr-xr-x - misc
-rw-r--r-- 9070 parser.ml
-rw-r--r-- 681 todo.org
-rw-r--r-- 23198 uiutils.ml
-rw-r--r-- 115 utf8syms.ml
-rw-r--r-- 7645 utils.ml
-rw-r--r-- 115 version.c
drwxr-xr-x - wsi