MIRA: tex-export still needed?
If yes, fix. If not, remove code from MIRA
(from redmine: issue id 2254, created on 2015-02-02, closed on 2016-01-19)
If yes, fix. If not, remove code from MIRA
(from redmine: issue id 2254, created on 2015-02-02, closed on 2016-01-19)