diff options
| author | herbelin | 2012-09-05 12:32:51 +0000 |
|---|---|---|
| committer | herbelin | 2012-09-05 12:32:51 +0000 |
| commit | 74cb9f996e6221f664f8a8b7b984c7a92e19bdf2 (patch) | |
| tree | fd58e60deea1f309b744dde5418f159358b74a52 /doc/refman/Program.tex | |
| parent | f0b936e7cb90000f5db6272b926cb13dc1a5c055 (diff) | |
A few fixes in configure file:
- Fixing parsing of option -custom
- More precise documentation of which option expects an argument
- Deprecation of obviously obsolete -emacs option
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15773 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/Program.tex')
0 files changed, 0 insertions, 0 deletions