summaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:01:05 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:01:05 +0200
commitc01be74d81a5466c58f8dc6c568db286b0979997 (patch)
treec386286c54374f25395013c3d8d6f3867e2fda1c /pretyping/pretyping.ml
parentb81f67debd8e75b481f2b5314c56c9876e9225a0 (diff)
update changelog
Diffstat (limited to 'pretyping/pretyping.ml')
0 files changed, 0 insertions, 0 deletions