diff options
| author | Gaëtan Gilbert | 2018-04-22 13:24:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-04-22 13:25:55 +0200 |
| commit | 2ded83ebfd958fd8187c11d4dec26af9d69e083c (patch) | |
| tree | 0b0e495c8b86f9596cfe60448f3ea5e154f2747f /kernel/uGraph.ml | |
| parent | dfbf22a098e8e2890d2e10da5d669d9960ef6771 (diff) | |
test suite Makefile: do not use %.stamp for subsystem targets
Diffstat (limited to 'kernel/uGraph.ml')
0 files changed, 0 insertions, 0 deletions