diff options
| author | Pierre-Marie Pédrot | 2014-12-17 18:21:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-12-17 18:21:25 +0100 |
| commit | 6aa2cd90c3091ebe397d83e1d70caa6237b4b551 (patch) | |
| tree | 873318058931a54d5a8cfc0fd555210a19604202 /kernel/names.ml | |
| parent | fba1f0ed91aff372234b5a95422ee18f1730522f (diff) | |
Fixing Makefile so that it puts the -thread flag on the right place.
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions