Zulip Chat Archive
Stream: new members
Topic: open command
Alex Zhang (May 24 2021 at 08:37):
What is the function of the open command? I saw open nat in a project file.
Kevin Buzzard (May 24 2021 at 08:38):
It just means that after open nat you can type foo instead of nat.foo
Kevin Buzzard (May 24 2021 at 08:39):
Check out chapter 6 of #tpil
Last updated: Dec 20 2023 at 11:08 UTC