From ada31c025335c6cc9228d3aed1476843edde58e6 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 8 Jun 2020 14:13:45 +0200 Subject: [PATCH] adjust \min font --- tex/iris.sty | 1 + 1 file changed, 1 insertion(+) diff --git a/tex/iris.sty b/tex/iris.sty index 269f26646..e3937c08b 100644 --- a/tex/iris.sty +++ b/tex/iris.sty @@ -86,6 +86,7 @@ \newcommand{\dom}{\textlog{dom}} \newcommand{\cod}{\textlog{cod}} \renewcommand{\lim}{\textlog{lim}} +\renewcommand{\min}{\textlog{min}} \newcommand{\Chains}{\textdom{Chains}} -- GitLab