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