]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/nlibrary/topology/convert.awk
...
[helm.git] / helm / software / matita / nlibrary / topology / convert.awk
index 68bcf8a6260599bc629c02f7081213fbe93635ec..757872324810787f3ff6a8cc89337fb4959a61b3 100644 (file)
@@ -9,6 +9,7 @@ BEGIN {
        match($0, "screenshot *\"([^\"]+)\"", data);
        key = data[1];
        refs[key] = key ".png"; 
+       $0 = gensub(/\(\*\* *screenshot[^*]*\*\)/,"",$0);
        }
 
 # literate programming