Code

Add a tips page to the book#881

Code

Draft

michaelpj wants to merge 7 commits intoplfa:devplfa/plfa.github.io:devfrom michaelpj:mpj/tipsmichaelpj/plfa.github.io:mpj/tipsCopy head branch name to clipboard

+199

Commits

Commits on Jun 2, 2023

• Add a tips page to the book

  Show description for 2bcaaf6
  michaelpj

  committed
  2bcaaf6

  Copy full SHA for 2bcaaf6

• [pre-commit.ci] auto fixes from pre-commit.com hooks

  Show description for bb65b2f
  pre-commit-ci[bot]

  committed
  bb65b2f

  Copy full SHA for bb65b2f

• Add to TOC

  michaelpj

  committed
  b9fc504

  Copy full SHA for b9fc504

Commits on Jun 3, 2023

• Merge branch 'dev' into mpj/tips

  wenkokke

  authored
  60a70fd

  Copy full SHA for 60a70fd

Commits on Jun 4, 2023

• Merge branch 'dev' into mpj/tips

  wenkokke

  authored
  befb33e

  Copy full SHA for befb33e

• Add epub-type

  wenkokke

  committed
  7b76e44

  Copy full SHA for 7b76e44

• Merge branch 'dev' into mpj/tips

  wenkokke

  authored
  052b456

  Copy full SHA for 052b456