From 1a6314a15567f05eba820ead48fc542c50296cfd Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Wed, 20 Jun 2018 13:27:19 +0200 Subject: [PATCH] Restored /about/ page, made minor revisions of /about/ page. --- README.md | 30 ++++++++++-------------------- _includes/header.html | 2 +- 2 files changed, 11 insertions(+), 21 deletions(-) diff --git a/README.md b/README.md index dbb4b8e0..223ca57a 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ material in a different way; see the [Preface](Preface). ## How to host literate code -In directory `sf/` run the following: +In directory `plta/` run the following: $ make clobber (remove all files before rebuilding system) $ make macos-setup (might need sudo, but try it without first) @@ -30,12 +30,6 @@ The visible page appears at localhost:4000/sf/ - - ## Unicode abbreviations @@ -43,32 +37,28 @@ The visible page appears at \u+ ⊎ \all ∀ \x × - x\_1 x₁ - x\_i xᵢ + x\_1 x₁ + x\_i xᵢ -Also see [here]( -https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194 -). +See [agda-input.el](https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194) for more details. -## Bindings for Agda mode +## How to use `agda-mode` ? create hole {!...!} create hole - C-c C-l reload + C-c C-l load buffer C-c C-c x split on variable x C-c C-space fill in hole -Also see [here]( -http://agda.readthedocs.io/en/latest/tools/emacs-mode.html -). +See [the emacs-mode docs]( http://agda.readthedocs.io/en/latest/tools/emacs-mode.html) for more details. ## Markdown -For markdown commands see [Daring Fireball]( +For an overview of the Markdown syntax, see [the original description]( https://daringfireball.net/projects/markdown/syntax -), [CommonMark]( +), [the CommonMark project]( http://spec.commonmark.org/0.28/ -), or [Kramdown]( +), or [the version that is used in this book]( https://kramdown.gettalong.org/syntax.html ). diff --git a/_includes/header.html b/_includes/header.html index 63e99636..1d2e0671 100644 --- a/_includes/header.html +++ b/_includes/header.html @@ -15,7 +15,7 @@