#pragma section-numbers off This is the chapter of the MemberManual that describes the bare minimum that you need to know concerning our use of DomTool. '''Why does this page exist? Why not point directly to DomTool/UserGuide? --AdamChlipala''' [[TableOfContents]] * Write to ~/.domtool. Explain how to make public or private. '''(Now covered appropriately in DomTool/UserGuide, IMO. --AdamChlipala)''' * Explain how to add a domain. In particular, an example, with content then annotated below. Point to relevant DomTool subpage for more. '''(Doesn't DomTool/UserGuide do this already? There is no concept of "adding a domain" at the rank-and-file-member level. You just write a Domtool source file that mentions a domain that you've been granted permission to use. --AdamChlipala)''' * Explain how to remove a domain. '''(Now covered appropriately in DomTool/UserGuide, IMO. --AdamChlipala)'''