diff options
| author | Pierre-Marie Pédrot | 2019-02-04 15:03:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 15:03:07 +0100 |
| commit | 4fdbf900e11f318f772dd1d81b5fa0a00ccaaa42 (patch) | |
| tree | 2b9218c9860f7e932ba3a08f7804362dea9cbc7d /engine/termops.ml | |
| parent | 79c87ab3ec6e41bbc5fe2cc43edcb4b934b81e46 (diff) | |
| parent | 6ec771e10c5af489d8529feea8fdc00beb21a855 (diff) | |
Merge PR #9437: Comment universe operations in Classes.context
Reviewed-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'engine/termops.ml')
0 files changed, 0 insertions, 0 deletions