diff options
author | 2004-07-17 23:41:17 +0000 | |
---|---|---|
committer | 2004-07-17 23:41:17 +0000 | |
commit | 04c838a604255c8b79425b731daa006047275da5 (patch) | |
tree | c3f0a5f3d2ef3e9559067d7ab95ed4fb25720443 /ide/coqide.ml | |
parent | 97cc3f9bb7f50a9d38494b3a4c5fa78384f1cf79 (diff) |
Try to build in opt, ready for dpatch, manpages added (but not used yet).
Diffstat (limited to 'ide/coqide.ml')
0 files changed, 0 insertions, 0 deletions