From 380a425a81e471bc974319af35cf63105485834b Mon Sep 17 00:00:00 2001
From: David Gauchard <gauchard@laas.fr>
Date: Wed, 28 Aug 2019 13:45:33 +0200
Subject: [PATCH] fix arduino builder command line
---
tools/build.py | 1 +
1 file changed, 1 insertion(+)
diff --git a/tools/build.py b/tools/build.py
index 828b53408e..34197e0ce0 100755
--- a/tools/build.py
+++ b/tools/build.py
@@ -57,6 +57,7 @@ def compile(tmp_dir, sketch, cache, tools_dir, hardware_dir, ide_path, f, args):
if args.debug_port and args.debug_level:
cmd += 'dbg={debug_port},lvl={debug_level}'.format(**vars(args))
cmd += ' '
+ cmd += '-built-in-libraries "' + ide_path + '/libraries" '
cmd += '-ide-version=10607 '
cmd += '-warnings={warnings} '.format(**vars(args))
if args.verbose: