Change to the directory that contains bootstrap.sh
tree07df17ae6d5e0f62bbbf6c18fd8e31a4e2a38106
-rw-r--r-- 52 .dir-locals.el
-rw-r--r-- 194 .gitignore
-rw-r--r-- 12 .merlin
-rw-r--r-- 32 .ocp-indent
-rw-r--r-- 996 BUILDING
-rw-r--r-- 50 INSTALL
-rw-r--r-- 8128 KEYS
-rw-r--r-- 468 README
-rw-r--r-- 792 Thanks
-rwxr-xr-x 7279 build.sh
-rw-r--r-- 62501 config.ml
-rw-r--r-- 353 diag.h
-rw-r--r-- 11843 glfont.c
-rw-r--r-- 176 keys.ml
-rw-r--r-- 66966 keysym2ucs.c
drwxr-xr-x - lablGL
-rw-r--r-- 117403 link.c
-rw-r--r-- 193037 main.ml
-rw-r--r-- 25902 main_osx.m
drwxr-xr-x - man
drwxr-xr-x - misc
-rw-r--r-- 9197 parser.ml
-rw-r--r-- 1933 todo.org
-rw-r--r-- 8299 utils.ml
-rw-r--r-- 1597 wsel.c
-rw-r--r-- 1611 wsi.mli
drwxr-xr-x - wsi