...

diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk
index e38f341edb0a3122f09b2f5ad48077d768e138a4..c881c0966520b9e5b8aa22c9f7f16af7f1dd4c89 100644 (file)
--- 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"