From 126dec5ed508673b821c0c9f5e242b897e287922 Mon Sep 17 00:00:00 2001
From: Giovanni Bussi <giovanni.bussi@gmail.com>
Date: Wed, 4 Jun 2014 11:48:33 -0400
Subject: [PATCH] Fix in manual
there where random "@" appearing here and there. Fixed now
---
user-doc/extract | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/user-doc/extract b/user-doc/extract
index 538665eca..89e74825a 100755
--- a/user-doc/extract
+++ b/user-doc/extract
@@ -229,5 +229,5 @@ cat $file.txt |
/^ *@TOOLS@ *$/r automatic/TOOLS.list
/^ *@MODULES@ *$/r automatic/modules.list
/^ *@CODES@ *$/r automatic/codes.list
-" | grep -Ev '^ *"@[A-Z]*@" *$' > ${file}PP.txt
+" | grep -Ev '^ *@[A-Z]*@ *$' > ${file}PP.txt
done
--
GitLab