diff options
| author | Pierre-Marie Pédrot | 2019-12-09 13:08:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-09 13:08:17 +0100 |
| commit | d7f493c25a3b1135a4b5b50d85b1d1b4b5ab1b21 (patch) | |
| tree | 63042397e88d18c1253f5bf1acf0ffa772a7c94b /kernel/genOpcodeFiles.ml | |
| parent | 1f4f00062b83b88114657223895bb1a367bc3cff (diff) | |
| parent | a260001e9119da2b07091303139c1db07bfed6ea (diff) | |
Merge PR #11234: [ide] Don't use -linkall for the GUI app.
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions