Lint fail: `replace() takes no keyword arguments`

Stream: mathlib4

[Alex Keizer]

The lint-style CI is failing on my job with a

 TypeError: replace() takes no keyword arguments

This seems like an issue with the script, rather than my commit being wrong, any ideas how to fix it?

[Julian Berman]

#7100

[Julian Berman]

That said I didn't read the code really at all but I think you should double check your branch as well, I think my 13 second glance is that your code has a minor style issue and the exception is just hiding telling you that nicely. I.e. check you have center dots instead of lower ones.

[Alex Keizer]

Ah, I indeed had regular dots instead of center dots. Weirdly enough, both #lint and a local make lint were not complaining about those

[Alex J. Best]

make lint does not run the style linter (perhaps it should), that needs to be run separately with ./scripts/lint-style.sh

[Alex J. Best]

Also sorry for the bad script, the third PR in the series #6569 would have fixed this also, and also made CI suggest the fix to you, but it's held up by my lack of time :wink:

[Alex Keizer]

Ah, is there one all-encompassing "check my PR for me" command? Or are there things that make lint checks but the script doesn't?

[Alex J. Best]

Unfortunately not right now (other than pushing a branch to github). make lint should more or less just do the equivalent of putting #lint at the bottom of all files.