Summary
- clarified error;
The file was modified | src/Pure/Thy/thy_header.ML (diff) |
The file was modified | src/Pure/Thy/thy_header.scala (diff) |
The file was modified | src/Pure/Thy/thy_header.ML (diff) |
The file was modified | src/Pure/Thy/thy_header.scala (diff) |