diff options
| author | Hugo Herbelin | 2017-01-04 19:15:26 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-01-04 19:18:45 +0100 |
| commit | 11bdfe88061c5bda160baec625b862a146809024 (patch) | |
| tree | 3ec8a6b29b818184f8aee7cf367c67ee642dfbbc /doc/tutorial/Tutorial.tex | |
| parent | ac9b9415e884dc478b1776b8792c690f61efd5ed (diff) | |
Fixing another inconsistency when looking for camlp5o when camlp5dir is given.
This was not fixed by b9a15a390f yet.
Diffstat (limited to 'doc/tutorial/Tutorial.tex')
0 files changed, 0 insertions, 0 deletions