diff --git a/stamp-vc b/stamp-vc new file mode 100644 index 0000000000000000000000000000000000000000..093711c197e5bade361b2b9e105fdea2f68594b6 --- /dev/null +++ b/stamp-vc @@ -0,0 +1 @@ +Stamp file to show that we are not in a distribution tarball (i.e., dune-autogen.sh needs to be called).