[Merged by Bors] - chore: fix backtick in docs

[int-y1]

I wrote a script to find lines that contain an odd number of backticks

---

[eric-wieser]

FWIW, I think this is legal markdown and renders correctly; but I think this change is fine.

[eric-wieser]

bors merge

Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style

[urkud]

Did you use something more advanced than this?

git grep '^\([^`]*`[^`]*`\)*`[^`]*$'  | grep -v '```'

[int-y1]

@urkud I wrote a 20-line python script

import os

def f(rootdir,pre):
    for root, subdirs, files in os.walk(rootdir):
        for fn in files:
            filepath=root+'\\'+fn
            with open(filepath) as f:
                a=pre+filepath[len(rootdir):].replace('\\','/')
                b=f.read()
                for i,s in enumerate(b.split('\n')):
                    s=s.strip()
                    if s.count('`')%2==0: continue
                    if s.count('`')==3 and '```' in s: continue
                    print(f'{a}:{i+1} {s}')

f('D:\\repo\\lean\\mathlib4\\Mathlib','Mathlib')
f('D:\\repo\\lean\\mathlib4\\test','test')
f('D:\\repo\\lean\\mathlib4\\Cache','Cache')
#f('D:\\repo\\lean\\mathlib4\\scripts','scripts')

Unfortunately, this script fetches ~1000 lines of macro code that I don't care about