diff options
| author | filliatr | 2000-01-26 23:40:56 +0000 |
|---|---|---|
| committer | filliatr | 2000-01-26 23:40:56 +0000 |
| commit | 726edc7a9dfaac6862dd071e8c7e6c0df56562d5 (patch) | |
| tree | e175444c327c2c788cdad3d7e7da9aff5fe40397 /dev | |
| parent | d56cc2ca71eee52a26f401ad2b37b8d9e6019a3c (diff) | |
lorsque ocamlc est donne a la main, alors ocamlopt est positionne avec
le mem chemin (et le suffixe eventuel .opt est conserve)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@285 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions