diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-07-26 20:00:07 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-07-26 20:01:06 +0200 |
| commit | 324a90078a47e469e4b185cfc6333a741cf48dc2 (patch) | |
| tree | 71724e024f1156741ddd1d9bd73dbe1033b38112 /ide/document.ml | |
| parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) | |
Enrich test file 4720.v with a compilation test of the extracted code
Diffstat (limited to 'ide/document.ml')
0 files changed, 0 insertions, 0 deletions