From cb5a7425740b458d6becf494f3989b76d8891dc8 Mon Sep 17 00:00:00 2001
From: "Edward Z. Yang" <ezyang@cs.stanford.edu>
Date: Sun, 11 Nov 2018 17:04:07 -0500
Subject: [PATCH] Replace flush.php with a shell script, to appease #192

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>
---
 maintenance/flush.php | 30 ------------------------------
 maintenance/flush.sh  |  8 ++++++++
 2 files changed, 8 insertions(+), 30 deletions(-)
 delete mode 100644 maintenance/flush.php
 create mode 100755 maintenance/flush.sh

diff --git a/maintenance/flush.php b/maintenance/flush.php
deleted file mode 100644
index c0853d23..00000000
--- a/maintenance/flush.php
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/usr/bin/php
-<?php
-
-chdir(dirname(__FILE__));
-require_once 'common.php';
-assertCli();
-
-/**
- * @file
- * Runs all generation/flush cache scripts to ensure that somewhat volatile
- * generated files are up-to-date.
- */
-
-function e($cmd)
-{
-    echo "\$ $cmd\n";
-    passthru($cmd, $status);
-    echo "\n";
-    if ($status) exit($status);
-}
-
-$php = empty($_SERVER['argv'][1]) ? 'php' : $_SERVER['argv'][1];
-
-e($php . ' generate-includes.php');
-e($php . ' generate-schema-cache.php');
-e($php . ' flush-definition-cache.php');
-e($php . ' generate-standalone.php');
-e($php . ' config-scanner.php');
-
-// vim: et sw=4 sts=4
diff --git a/maintenance/flush.sh b/maintenance/flush.sh
new file mode 100755
index 00000000..65ef6f8c
--- /dev/null
+++ b/maintenance/flush.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+set -ex
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
+php "$DIR/generate-includes.php"
+php "$DIR/generate-schema-cache.php"
+php "$DIR/flush-definition-cache.php"
+php "$DIR/generate-standalone.php"
+php "$DIR/config-scanner.php"