Revision 384ee08a
ref #7470 add verbatim type designation / TextTypeDesignation
Files
- added
- modified
- copied
- renamed
- deleted
ID | 384ee08ae00cf3a8bf510a8af5ca179d6213022d |
Parent | 71d214d3 |
Child | 60f82184 |
Added by Andreas Müller almost 2 years ago
ref #7470 add verbatim type designation / TextTypeDesignation