aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorHugo Herbelin2016-05-04 11:15:37 +0200
committerHugo Herbelin2016-05-04 11:17:45 +0200
commit796859aca4fc85dc721b670d95b0c2aaace55e32 (patch)
tree7cf8f5b32dcaffe57143aa08830dfadf3f47573d /kernel
parent78e616d56dc0646d0c67ab57e11671a6c08d0cc7 (diff)
Fixing subst.out after changing spacing in goal output (24a125b77).
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions