Unfortunately, we lost some old, long unsused repositories recently. You can restore them by creating a new, empty repository in the project view and then pushing there using something like for x in $(git branch -r | grep -v HEAD); do git push origin $x:refs/heads/${x#*/}; done; git push --tags

The SSH username for accessing EduGit changed: Please update your remotes to use git@ instead of gitlab@.

Verified Commit e2c92d39 authored by mirabilos's avatar mirabilos Committed by mirabilos

install the paper (with the caveat of being rudimentary)

parent 9dd500d1
......@@ -49,6 +49,7 @@ pages:
cp -r html public/
cp foils/the_m_irabilos.png public/foils/
cp notes/*.htm public/notes/
cp tex/workshop.pdf public/
sed 's!\\.\\./!!g' <build/pages-stub.htm >public/index.html
.PHONY: all run debug edit export show pdf linklist clean pages
......@@ -22,7 +22,8 @@
at EduGit. This is a stub site, but you can directly view my <a
href="../notes/linklist.htm">list of auxillary links</a> here, as well
as a <a href="../html/index.html">rendered version of the slide deck</a>
(HTML with images, plain UTF-8 text is linked).</p>
(HTML with images, plain UTF-8 text is linked) and a (very rudimentary)
<a href="workshop.pdf">paper (PDF)</a>.</p>
<p>Legalities can be found in the aforementioned source repository.</p>
<h3><img src="../foils/the_m_irabilos.png" alt="mirabilos" title="mirabilos"
style="height:3ex;" /></h3>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment