From df120ac85b8d6870caf8b61b61a0103012f8ef64 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 22 Oct 2016 13:40:01 +0200
Subject: [PATCH] docs: add linkto website
---
docs/base-logic.tex | 2 +-
docs/iris.tex | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 5b15171f8..a88b58ad7 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -395,7 +395,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
\end{mathpar}
The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
-\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
+%\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
\subsection{Consistency}
diff --git a/docs/iris.tex b/docs/iris.tex
index 1157cfaaa..ca5b8ff16 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -18,7 +18,7 @@
\begin{document}
\title{\bfseries The Iris 2.0 Documentation}
-%\author{The Iris Team}
+\author{\url{http://plv.mpi-sws.org/iris/}}
\maketitle
\thispagestyle{empty}
--
GitLab