When KeY is started, there are multiple warnings about duplicate sort declarations in the taclet base. While we should get rid of those in the future, they are not severe, but may confuse the users. We should mark them as "Debug", such that they are suppressed for normal users.
Reproducible
always
Steps to reproduce
Start KeY (from a CLI).
Load any .key or .java file, such that parsing of the taclet library is triggered.
WolframPfeifer
commented
2 weeks ago
Description
When KeY is started, there are multiple warnings about duplicate sort declarations in the taclet base. While we should get rid of those in the future, they are not severe, but may confuse the users. We should mark them as "Debug", such that they are suppressed for normal users.
Reproducible
always
Steps to reproduce
On the CLI, the warnings described above appear.