diff --git a/build_docs.pl b/build_docs.pl index a972cd9b0653..18eb554949fd 100755 --- a/build_docs.pl +++ b/build_docs.pl @@ -1,5 +1,5 @@ #!/usr/bin/env perl - +system("echo '====== Demo successful ======'"); # Flush on every print even if we're writing to a pipe (like docker). $| = 1;