max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: remove "section" keywords, which aren't highlighted

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-20 16:56:53 +01:00
parent 23bedc5ef5
commit 1e2c0d1d41
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
doc/highlight.js
View file

@ -1113,7 +1113,8 @@ hljs.registerLanguage("lean", function(hljs) {
'import open theory prelude renaming hiding exposing ' +
'calc match do by let in extends ' +
'fun assume ' +
'#check #eval #reduce #print',
'#check #eval #reduce #print ' +
'section namespace end',
built_in:
'Type Prop|10 Sort rw|10 rewrite rwa erw subst substs ' +
'simp dsimp simpa simp_intros finish ' +
@ -1134,8 +1135,6 @@ hljs.registerLanguage("lean", function(hljs) {
'tt ff',
meta:
'noncomputable|10 private protected meta mutual',
section:
'section namespace end',
strong:
'sorry admit',
};