mathport/Oneshot

Stream: mathlib4

[Antoine Chambert-Loir]

One suggestion to add to the Oneshot/README.md file : explain the role of the file Oneshot/lean3-in/leanpkg.pth

(After a first run of make oneshot, I wanted to do another one, and moved all the files there to another location, and nothing worked then, so that I reinstalled mathport again and finally understood what had went wrong…)

[Scott Morrison]

@Antoine Chambert-Loir, does this look okay? I'll merge on the basis of a thumbs-up. :-)