fix create_dist

fblanqui · Mar 18, 2021 · d1929ff · d1929ff
1 parent 4c2cc10
commit d1929ff
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/create_dist b/create_dist
@@ -55,7 +55,7 @@ dir=color.$version
 rm -rf $dir
 cp -r color $dir
 rm -rf $dir/Coccinelle $dir/Conversion/Coccinelle.v
-head -n -3 color/README > $dir/README
+head -n -3 color/README.md > $dir/README.md
 create_tar_gz
 md5sum $cwd/$dir.tar.gz