diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-10 23:35:47 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 11:15:31 +0200 |
| commit | 5b506165097047aa8b6b431db9f2cbc8dbf6c3de (patch) | |
| tree | 42db993ebdee049de57f155d4977470c969c8f1e /ide/minilib.ml | |
| parent | 615047314c4e3331db09883b30c067544a03023b (diff) | |
Unifying the layout of installation directories.
There seems to have been several bugs, when -prefix is given:
- Under win32: "" instead of "lib" (presumably introduced in ab442aed8, 2006)
- Under win32: datadir, mandir, docdir should presumably be in
"share", "man", "doc", as given in default
- Under non-win32: coqdoc files should be in latex subdir not emacs subdir
Diffstat (limited to 'ide/minilib.ml')
0 files changed, 0 insertions, 0 deletions