diff options
| author | Jim Fehrle | 2018-08-25 17:00:55 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-08-30 15:45:59 -0700 |
| commit | 81b5103d5afeb6ae200f922a43f39c47525b36a2 (patch) | |
| tree | 4b870584b7c4753957abda2b2232256f2def577b /kernel/nativecode.ml | |
| parent | bf1446294dba45d3ea9b7bb39d2fc96617848c03 (diff) | |
Replace use of xargs in "make clean", which tends to fail on Windows/Cygwin.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions