@mgudemann Mh, good point.

I wonder, whether regular expressions might still work, by using greedy expressions, and matching *before* `File ` instead of after.