diff options
| author | Gaëtan Gilbert | 2018-11-28 12:48:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-28 12:49:43 +0100 |
| commit | 8ea2e4100737794d3130e2bc341f5a1c6422082f (patch) | |
| tree | 59368077c9350c1a8d25b84abeba5402cba1c781 /dev/include | |
| parent | 2e36fbcac4a04d4f29925ba09f441db6426b7af1 (diff) | |
coqide: Remove unused win32_kill C function
Unused since b0da879dc6abfca6b4e233b7469265a5cf52ce15 (see also
followup 4f554c88aa).
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions