From a1843fa495c952f91e330b7572e6ea214fff5d5c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 8 Dec 2008 09:34:40 +0000 Subject: [PATCH] better replacement for \\def --- helm/software/matita/help/C/scripts/fix-symbols.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/help/C/scripts/fix-symbols.sh b/helm/software/matita/help/C/scripts/fix-symbols.sh index ed45fce9a..eb491489a 100755 --- a/helm/software/matita/help/C/scripts/fix-symbols.sh +++ b/helm/software/matita/help/C/scripts/fix-symbols.sh @@ -1,4 +1,4 @@ #!/bin/sh -sed -i 's/\\&\\#x225d;/:=/g' $1 +sed -i 's/\\&\\#x225d;/\\ensuremath{\\stackrel{def}{=}}/g' $1 sed -i 's/\\&\\#x3a9;/\\ensuremath{\\Omega}/g' $1 -- 2.39.2