diff options
| author | Gaëtan Gilbert | 2018-06-23 15:00:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 12:03:10 +0200 |
| commit | fb9003c7850c459d7a5981212d8ef87de877bd9f (patch) | |
| tree | 463bb0753a912ea2d0a7ab59518de820e20429a2 /dev | |
| parent | 4ab54f3cca76632cb6e258c84abc259e15e9e9f8 (diff) | |
Move Heads to pretyping (is_projection will move to Recordops)
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions