Admin/PIDE/convert
changeset 53498 05313b45a5ae
parent 46245 01496117a5cc
--- a/Admin/PIDE/convert	Tue Sep 10 11:46:51 2013 +0200
+++ b/Admin/PIDE/convert	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 THIS="$(cd "$(dirname "$0")"; pwd)"
 SUPER="$(cd "$THIS/.."; pwd)"