aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vio_checking.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-05 10:38:36 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-05 10:38:36 +0100
commitd403b2200ef32afd1eb1087a1f0ef2e6b8bb93f6 (patch)
tree1fdf7b431f2351f9cc569011b06d458b3cfc25ee /stm/vio_checking.ml
parent423b7298535c88b14926e92a8763420c69f89f6d (diff)
parent8f47273f118808373649a3a084e4a3c99167edd3 (diff)
Merge PR #6266: Safe unmarshalling in the checker
Diffstat (limited to 'stm/vio_checking.ml')
0 files changed, 0 insertions, 0 deletions