diff options
| author | letouzey | 2009-02-27 14:37:51 +0000 |
|---|---|---|
| committer | letouzey | 2009-02-27 14:37:51 +0000 |
| commit | d298481418ca18736180df25bddaf303f5cf7fce (patch) | |
| tree | 8106a76f1f1b298bd7dc55ddcf0a89d656d0b0ae /dev/include | |
| parent | 8f363f638f4cd1fe86f42e202b9e405676a7b624 (diff) | |
Makefile: avoid building an empty contrib.cmxa
Patch suggested by Yves. Now that the list of contrib to link statically
in coqtop can be empty, we should avoid trying to build an empty
contrib.cmxa, since this fails at least on MacOS.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11947 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions