From 39f3d204452f82a8a4f7e68557d827f4fb747197 Mon Sep 17 00:00:00 2001
From: Norbert Renner <norbert.renner@gmx.de>
Date: Wed, 22 Jan 2020 10:59:48 +0100
Subject: [PATCH] Fix /usr/bin/sh not found on Ubuntu 18.04, using /bin/sh
 instead

---
 misc/scripts/generate_profile_variants.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/misc/scripts/generate_profile_variants.sh b/misc/scripts/generate_profile_variants.sh
index 584de69..c93dcda 100755
--- a/misc/scripts/generate_profile_variants.sh
+++ b/misc/scripts/generate_profile_variants.sh
@@ -1,4 +1,4 @@
-#!/usr/bin/sh
+#!/bin/sh
 cd "$(dirname "$0")"
 cd ../profiles2