diff options
| author | David Aspinall | 2004-02-07 19:31:13 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-02-07 19:31:13 +0000 |
| commit | b9caaa8e4b66817dbc66d0e79b567b3285869fea (patch) | |
| tree | c5420dac1aa1afc28168867ca5cc9c610a46399e /html/notes.txt | |
| parent | 87174e13a8aa064f6d00ef9248da9938ea4978f6 (diff) | |
Deleted file
Diffstat (limited to 'html/notes.txt')
| -rw-r--r-- | html/notes.txt | 56 |
1 files changed, 0 insertions, 56 deletions
diff --git a/html/notes.txt b/html/notes.txt deleted file mode 100644 index 7d73ce30..00000000 --- a/html/notes.txt +++ /dev/null @@ -1,56 +0,0 @@ -Developers' Notes about Web Pages ---------------------------------- - -NEW: server hacks needed to serve these pages, giving nice urls - - PHP3 module included - .html treated as application - - Mime magic configured: - -LoadModule mime_magic_module modules/mod_mime_magic.so -AddModule mod_mime_magic.c -MimeMagicFile /etc/httpd/conf/magic - -to recognize files beginning <?php, by - adding this to /etc/httpd/conf/magic: - -0 string <?php application/x-httpd-php3 - -Then add these links: - - news -> index.html - doc -> index.html - -etc. - -*************** - -Notes about php: - -Some functions I've written - - <?php hlink("html file","text","status message")?> - -NB: no space after text so you must write - - <?php ... ?> blah - -to get a space. Don't put "blah" onto a new line, space will -be lost! - - -************* - -Tell Thomas (& other folk?) to update his home page links to Proof General. -[Probably okay: Thomas links to image in home directory, but we'll - keep that as a copy of images/ProofGeneral.jpg] - -************* - -Suggestions for improving web pages after Rod reading them: - - - slideshow rather than single screen shot - - separate feature list - - explain what a proof script is and what script management buys you - |