Merge branch 'develop' into dynamic-shell-command-registration

This commit is contained in:
angelos-oikonomopoulos 2018-06-12 13:26:42 +02:00 committed by GitHub
commit 0aea8efb7c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -5,7 +5,7 @@ RUN apt-get update && \
apt-get install -y --no-install-recommends \
build-essential doxygen git wget unzip python-serial python-pip \
default-jdk ant srecord iputils-tracepath rlwrap \
mosquitto mosquitto-clients \
mosquitto mosquitto-clients gdb \
&& apt-get clean
# Install ARM toolchain