diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-26 13:41:56 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-26 13:41:56 +0000 |
| commit | 1cd5872ca94f1b3c998850646b1f101394aa6bad (patch) | |
| tree | 3911f5cd79fcb9ccf5758edc1555a932d9b7c87c /Makefile | |
| parent | 5bcc4bbe41762856c1406c2cde12f57659dd046f (diff) | |
Add -makecmd configure option
This allows choosing gmake on *BSD (patch from Nima Hoda).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12689 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions