From 8f08d41fcefb66be89b23e56d309610cd2d1dae4 Mon Sep 17 00:00:00 2001
From: regnat <rg@regnat.ovh>
Date: Tue, 11 Apr 2017 14:56:20 +0200
Subject: [PATCH] Change the \orthplus symbol to a diamond

The old one was ugly ond too big
---
 common/header.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/common/header.tex b/common/header.tex
index 28d1ffb..6d57fe7 100644
--- a/common/header.tex
+++ b/common/header.tex
@@ -72,7 +72,7 @@
 \DeclareMathOperator\dom{dom}
 \DeclareMathOperator\deff{def}
 \newcommand{\orthsum}{\oplus^\bot}
-\newcommand{\orthplus}{\overset{\bot}{+}}
+\newcommand{\orthplus}{\diamond}
 \newcommand{\subtype}{\leq}
 \newcommand{\onerec}{\{ \textbf{..} \}}
 \DeclareCollectionInstance{plainmath}{xfrac}{mathdefault}{math}