From ae98d4aa397016e15ce2e2f8ba455322712157ec Mon Sep 17 00:00:00 2001
From: Gilles Peskine <Gilles.Peskine@arm.com>
Date: Tue, 10 Oct 2017 11:26:45 +0200
Subject: [PATCH] Minor style fix

---
 scripts/config.pl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/config.pl b/scripts/config.pl
index b99140a37..5a06a3338 100755
--- a/scripts/config.pl
+++ b/scripts/config.pl
@@ -215,7 +215,7 @@ for my $line (@config_lines) {
     }
 
     if (defined $config_write) {
-        print $config_write $line or die "write $config_file: $!\n";;
+        print $config_write $line or die "write $config_file: $!\n";
     }
 }