|
Size: 885
Comment: Comments
|
Size: 923
Comment: Mention changes to DomTool/UserGuide
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 9: | Line 9: |
| * Write to ~/.domtool. Explain how to make public or private. '''(Add to DomTool/UserGuide instead. --AdamChlipala)''' | * Write to ~/.domtool. Explain how to make public or private. '''(Now covered appropriately in DomTool/UserGuide, IMO. --AdamChlipala)''' |
| Line 11: | Line 11: |
| * Explain how to remove a domain. '''(Add to DomTool/UserGuide instead. --AdamChlipala)''' | * Explain how to remove a domain. '''(Now covered appropriately in DomTool/UserGuide, IMO. --AdamChlipala)''' |
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
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)