diff options
| author | Pierre-Marie Pédrot | 2020-06-08 19:20:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | c00a369a8bd70efad3e1481daa78ab483038c6cb (patch) | |
| tree | 2609e819b12dc26991df5bad1623c1e486b1c63b /Makefile.dev | |
| parent | 9eca7cca68dc82aa738a8d408d75e1b9b5405646 (diff) | |
Move the hint polymorphic status to the hint instance.
It is only used for this kind of hints, never for Extern / Unfold.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions