|
⇤ ← Revision 1 as of 2007-10-25 00:07:09
Size: 424
Comment: Initial contents
|
Size: 885
Comment: Comments
|
| 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. '''(Add to DomTool/UserGuide instead. --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. '''(Add to DomTool/UserGuide instead. --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. (Add to DomTool/UserGuide instead. --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. (Add to DomTool/UserGuide instead. --AdamChlipala)