diff --git a/ci/after_success.sh b/ci/after_success.sh
index 5c3873f83d..cd86144d65 100755
--- a/ci/after_success.sh
+++ b/ci/after_success.sh
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 # This runs only when a commit is pushed to master. It is responsible for
 # updating docs and computing coverage statistics.