Bugfix RPi gpio export

When restarting the sample service the script for
exporting output gpios exited with errors and
the service was never started.
This is fixed by only exporting gpios if they are
not already exported.

src/ports/linux/enable-rpi-gpio-pins.sh

@@ -1,7 +1,14 @@
 #!/bin/sh
 
+# Avoid exporting gpios several times
+gpio_export() {
+    if ! [ -d /sys/class/gpio/gpio$1 ]; then
+        echo $1 > /sys/class/gpio/export
+    fi
+}
+
 # Enable GPIO pins for digital inputs (buttons) on Raspberry Pi
-echo 22 > /sys/class/gpio/export
-echo 27 > /sys/class/gpio/export
+gpio_export 22
+gpio_export 27
 
 # GPIO pins for digital outputs (LEDs) are enabled in another script