diff options
| author | Gaëtan Gilbert | 2018-11-07 14:48:09 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-07 14:48:09 +0100 |
| commit | 965048aa0d4eef1d3933aeb7582c23c78ba838f7 (patch) | |
| tree | 3db191c64ffa9c342d9667abbbd417146d59f481 /plugins/syntax | |
| parent | 8f09c0667d2566534ab9da77651686904b23aac5 (diff) | |
| parent | c29eb307760086fb5951a1771a91c25360248852 (diff) | |
Merge PR #8901: [dune] Add "quick" and "check" targets for fast builds.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions