diff options
| author | Michael Soegtrop | 2018-05-19 11:38:16 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2018-05-19 11:38:16 +0200 |
| commit | 6ff355338986e87f37ad25bf9943ca42135357d6 (patch) | |
| tree | 0d368a2ee357e12bb23ea236808d85597613c1f2 /plugins | |
| parent | e0131a0038531ccc5f42fa84c79761a364b10dd7 (diff) | |
| parent | 1c5f120fba49b397aad7b8c07dcc10cec1cfc026 (diff) | |
Merge PR #7527: [windows] Don't build menhir and int anymore in the packaging scripts.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions