search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

Updated TeX packages #133

Closed GinoGiotto closed 1 year ago

GinoGiotto commented 1 year ago

This pull request does 3 things:

  1. Fix checks 1, 9, 13 of https://github.com/metamath/set.mm/issues/3091 by adding the accents package. There was a discussion about long term treatment of these packages, so this is to be considered a temporary solution to not obstruct the flow of https://github.com/metamath/set.mm/pull/3100 according to https://github.com/metamath/set.mm/issues/3091#issuecomment-1474327524 https://github.com/metamath/set.mm/pull/3099#issuecomment-1474323774

  2. Fix issue related to relative position between the amssymb and phonetic packages https://github.com/metamath/set.mm/pull/3090#issuecomment-1465046048

  3. Delete graphicx package since TeX substitutions with \rotate are now replaced with \riota in https://github.com/metamath/set.mm/pull/3099

GinoGiotto commented 1 year ago

Is it good to merge? Nobody said anything for more than 2 weeks @benjub

benjub commented 1 year ago

Is it good to merge? Nobody said anything for more than 2 weeks @benjub

LGTM, but it's up to @digama0 to merge if he deems it ok.

digama0 commented 1 year ago

I'm not super happy about not being able to validate changes like this in CI, but I don't have any better suggestion and the changes themselves look fine.