diff options
| author | Maxime Dénès | 2014-04-29 14:41:49 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-04-29 14:41:49 -0400 |
| commit | 6acf543800fe176ca7d47ef7165ebc14588efb6f (patch) | |
| tree | 1bf524ee47195cc4d3ebdd48113aaeeaf1bc5c1d /dev/base_include | |
| parent | 3b176883b7fcd9af6881ae1049bbd078c8d19577 (diff) | |
Native compiler: hide compiled files in a .coq-native subdirectory.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions