mirror of
https://git.lyx.org/repos/lyx.git
synced 2025-01-14 12:25:11 +00:00
a5a8c6731c
Comment from Jürgen Spitzmüller: As we didn't report makeindex errors until my commit yesterday(17 Dec 2019), this problem got unnoted (and the respective index entry was simply omitted).