How to download text files

A few of the plain text files in this archive are embedded in HTML to facilitate viewing as text. On the server, they actually have .html file name extensions, which are suppressed on archive directory pages (displayed from index.html files).

To download such a file as ASCII text, view it, and use the appropriate browser menu item to save it as text. Some browsers supply the file name from the title at the very top of the browser window, which is the name without the .html extension. Others include the extension, which you have to delete by hand.

With Netscape, you can also save a file as text after clicking on and holding its link. Then you do have to delete the .html extension by hand.

Files that have a visible .html extension on an index.html page are actually HTML, which you would save as text only if you wanted to lose the formatting.

Some of the other plain text files are made to view as text by giving them an extra .txt extension on the server, which is suppressed when viewing the directory index.html page. TeX source files are a good example. They may need to have the .txt extension deleted by hand as described above.

Last updated February 05, 2005.