From cc71d7571ad58f836e9ce92ce3034ea8a933ef50 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 22 Sep 2005 08:58:57 +0000
Subject: [PATCH] ...

---
 helm/matita/scripts/insert.awk | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk
index e38f341ed..c881c0966 100644
--- a/helm/matita/scripts/insert.awk
+++ b/helm/matita/scripts/insert.awk
@@ -1,6 +1,6 @@
  {
 	result=tolower($3);
-	if( $1 ~ "\.opt$" )
+	if( $1 ~ ".opt$" )
 		compilation="opt"
 	else
 		compilation="byte"
-- 
2.39.2