From 9fc2dbef702eb560fdc32b65ff7287eb503a4a7e Mon Sep 17 00:00:00 2001
From: carlocamilloni <carlo.camilloni@gmail.com>
Date: Wed, 2 Aug 2017 17:00:41 +0200
Subject: [PATCH] user-doc: fix some duplicated line [makedoc]
---
user-doc/extract | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/user-doc/extract b/user-doc/extract
index 6480ca0eb..1050e4df0 100755
--- a/user-doc/extract
+++ b/user-doc/extract
@@ -363,7 +363,7 @@ rm automatic/*.txte
rm -f *PP.txt *PP.md
-keywords=`grep "@[A-Z_]*@" *.md | awk -F"@" '{print $2}' | uniq`
+keywords=`grep "@[A-Z_]*@" *.md | awk -F"@" '{print $2}' | sort | uniq`
for f in *.txt *.md
do
--
GitLab