|
Size: 424
Comment: Initial contents
|
Size: 923
Comment: Mention changes to DomTool/UserGuide
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 5: | Line 5: |
| '''Why does this page exist? Why not point directly to DomTool/UserGuide? --AdamChlipala''' |
|
| Line 7: | Line 9: |
| * Write to ~/.domtool. Explain how to make public or private. * Explain how to add a domain. In particular, an example, with content then annotated below. Point to relevant DomTool subpage for more. * Explain how to remove a domain. |
* 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)''' |
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)