diff options
| author | Hugo Herbelin | 2015-02-24 18:44:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-24 18:58:19 +0100 |
| commit | 152f57925a6dc08ce3f332319b50eae9fb7bb622 (patch) | |
| tree | bdd7389595eee1b2009d85671992b9b1a7484131 /dev/base_include | |
| parent | f7b29094fe7cc13ea475447bd30d9a8b942f0fef (diff) | |
Calling coq references lazily in plugin cc so as to support static linking of plugins.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions