From 5221eb39f99fc87f839c2389c5185ed54a884045 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 30 Jan 2019 16:21:37 +0100
Subject: [PATCH] A note about the Iris LaTeX macros in the README.

Many people using Iris appear to not know these; this may make them
easier to find.
---
 README.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/README.md b/README.md
index 4ba0da9dd..e442d7870 100644
--- a/README.md
+++ b/README.md
@@ -126,3 +126,6 @@ that should be compatible with this version:
   [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which also
   requires an MPI-SWS GitLab account.
 * To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
+* If you are writing a paper that uses Iris in one way or another, you could use
+  the [Iris LaTeX macros](docs/iris.sty) for typesetting the various Iris
+  connectives.
-- 
GitLab