diff options
| author | Pierre-Marie Pédrot | 2015-09-06 13:20:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-06 13:20:32 +0200 |
| commit | 5080991902a05ee720ab1d6fa1c9d592d3ffd36c (patch) | |
| tree | 53b68887977933e834a16c91114846c05040dca3 /kernel/indtypes.ml | |
| parent | 26be4ca94f8ba0a03826a2df09491bb0d96d7363 (diff) | |
Adding a Makefile target for the MSets and MMaps directories.
The target creation process should eventually be automated, because it
is tedious and error-prone as witnessed by this commit.
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions