aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-28 12:58:00 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-28 12:58:00 +0200
commitbd8606189268c3fcdd3506872d459cb9032a33bf (patch)
tree413e691b7c6651d12f6f1f75782e3f76053eadfc /kernel
parent792042a695083b73f0e998b20197ef0d3de25812 (diff)
parent076efd5f8d17f1b73bcc7669641b89f86819e3c9 (diff)
Merge PR #7090: stm: don't propagate side effects when editing a proof
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions