Revision fbe910aa
ref #7829, ref #7800 improve nom. ref. matcher (also changes the result type => needs adaptation in client Apps)
Files
- added
- modified
- copied
- renamed
- deleted
| ID | fbe910aa737105de0cb24ea5ca58109558faf077 |
| Parent | 269cc178 |
| Child | b3d38029 |
Added by Andreas Müller 7 months ago
ref #7829, ref #7800 improve nom. ref. matcher (also changes the result type => needs adaptation in client Apps)