diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-08 18:35:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-08 18:42:50 +0200 |
| commit | 007ab31b4d1b9457d2758a614aed5a49dee53b62 (patch) | |
| tree | 59044dde6e53ee4e812cca72e979a11d4069101f /dev | |
| parent | 48c44b55b76e75aa2af9f82753c6ffe7531790c8 (diff) | |
Fixing #5460 (limitation in computing deps in pattern-matching compilation).
This was assuming dependencies occurring in configurations of
the form x:A, y:B x, z:C x y |- match x, y, z with ... end".
But still work to do for better management of dependencies in general...
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions