Philip Chimento f00dd1a594 Integration settings for Linux ... I'll keep my inform7-ide checkout in the same root as inform, and it's now named inform7-ide rather than gnome-inform7. (Later I may change this to install directly into /usr though.)		2022-04-26 22:54:15 -07:00
..
Changes	Adapted indoc slightly for documentation on new website	2019-06-26 09:05:27 +01:00
Documentation	Integration settings for Linux	2022-04-26 22:54:15 -07:00
Imagery	Renamed image to remove spurious space in filename	2022-04-19 12:15:22 +01:00
Outcome Pages	Reorganised main inform repository	2019-03-16 13:12:11 +00:00
Sample Projects	Reorganised main inform repository	2019-03-16 13:12:11 +00:00