diff options
| author | Emilio Jesus Gallego Arias | 2018-03-03 01:50:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-06 10:53:27 +0100 |
| commit | 6e0c7f83c6ad024df7105f9b799fda9dbe7a14d0 (patch) | |
| tree | 92bccad12e3f512b31568ba6d422420f956398d8 /dev/base_include | |
| parent | db8fcbb7763ac784f7c72b72509d5dc7c2c5323c (diff) | |
[compat] Remove "Discriminate Introduction"
Following up on #6791, we the option "Discriminate Introduction".
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions