Merge branch 'master' into master

dhlorenz · May 18, 2024 · bf7a682 · bf7a682
2 parents 72303df + 13ea840
commit bf7a682
Show file tree

Hide file tree

Showing 5 changed files with 106 additions and 4 deletions.
diff --git a/.github/workflows/jekyll-pages.yml b/.github/workflows/jekyll-pages.yml
@@ -0,0 +1,50 @@
+name: Deploy Jekyll with GitHub Pages dependencies preinstalled
+
+on:
+  # Runs on pushes targeting the default branch
+  push:
+    branches: ["master"]
+
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
+# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
+
+jobs:
+  # Build job
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+      - name: Setup Pages
+        uses: actions/configure-pages@v5
+      - name: Build with Jekyll
+        uses: actions/jekyll-build-pages@v1
+        with:
+          source: ./
+          destination: ./_site
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v3
+
+  # Deployment job
+  deploy:
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4
diff --git a/Material/Tutorials/sml/errors.md b/Material/Tutorials/sml/errors.md
@@ -103,9 +103,7 @@ fun f (a:{s: int, r: int}) = {s: (#s a), r: (#r a)};
 ```
 <!-- .element: data-thebe-executable-sml data-language="text/x-ocaml" -->
 
-NOTE: `:` denotes type, we need to use `=` in the returned expression to denote a value. another common error:
-`{{(#s a), (#r a)}}`
-?? ?? ??
+NOTE: `:` denotes type, we need to use `=` in the returned expression to denote a value. another common error: `{(#s a), (#r a)}`
 
 <!--vert-->
 

diff --git a/_config.yml b/_config.yml
@@ -1,5 +1,5 @@
 title: PL
-description: 236319 Spring 2024, Prof. Lorenz
+description: 236319 Spring 202x, Prof. Lorenz
 show_downloads: false
 google_analytics:
 theme: jekyll-theme-tactile

diff --git a/_includes/footer.html b/_includes/footer.html
@@ -0,0 +1 @@
+D. H. Lorenz
diff --git a/_layouts/default.html b/_layouts/default.html
@@ -0,0 +1,53 @@
+<!DOCTYPE html>
+<html lang="{{ site.lang | default: "en-US" }}">
+  <head>
+    <meta charset='utf-8'>
+    <meta name="viewport" content="width=device-width, initial-scale=1">
+    <meta http-equiv="X-UA-Compatible" content="IE=edge">
+    <link rel="stylesheet" href="{{ '/assets/css/style.css?v=' | append: site.github.build_revision | relative_url }}">
+    <link rel="stylesheet" type="text/css" href="{{ '/assets/css/print.css' | relative_url }}" media="print">
+    <!--[if lt IE 9]>
+    <script src="//html5shiv.googlecode.com/svn/trunk/html5.js"></script>
+    <![endif]-->
+
+{% seo %}
+    {% include head-custom.html %}
+  </head>
+
+  <body>
+    <div id="container">
+      <div class="inner">
+
+        <header>
+          <h1>{{ page.title | default: site.title | default: site.github.repository_name }}</h1>
+          <h2>{{ page.description | default: site.description | default: site.github.project_tagline }}</h2>
+        </header>
+        <section id="downloads" class="clearfix">
+          {% if site.show_downloads %}
+          <a href="{{ site.github.zip_url }}" id="download-zip" class="button"><span>Download .zip</span></a>
+          <a href="{{ site.github.tar_url }}" id="download-tar-gz" class="button"><span>Download .tar.gz</span></a>
+          {% endif %}
+	{% if site.github.public %}
+	  {% if site.github.is_project_page %}
+          <a href="{{ site.github.repository_url }}" id="view-on-github" class="button"><span>View on GitHub</span></a>
+	  {% else %}
+          <a href="{{ site.github.owner_url }}" id="view-on-github" class="button"><span>View on GitHub</span></a>
+	  {% endif %}
+	{% endif %}
+        </section>
+        <hr>
+        <section id="main_content">
+          {{ content }}
+        </section>
+
+        <footer>
+        {% if site.github.is_project_page %}
+          {{ site.title | default: site.github.repository_name }} is maintained by <a href="{{ site.github.owner_url }}">{{ site.github.owner_name }}</a><br>
+        {% endif %}
+          This page was generated for 236319 Spr 2023.
+        </footer>
+
+      </div>
+    </div>
+  </body>
+</html>