diff options
| author | Enrico Tassi | 2017-08-29 13:54:46 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-08-29 17:47:57 +0200 |
| commit | a93279fb7fe5917ab859e7b3dfb6f89522161419 (patch) | |
| tree | aeec78aa7cf69075e631fcd247fd4141d81beddc /dev/include | |
| parent | 6e07e3a53e56882043b9db49f03fdf1470a16c46 (diff) | |
coq_makefile: print error message when coqlib is not set properly
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions