diff options
Diffstat (limited to 'Tools')
| -rwxr-xr-x | Tools/px_generate_uorb_topic_headers.py | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Tools/px_generate_uorb_topic_headers.py b/Tools/px_generate_uorb_topic_headers.py index 54430cc38..4bcab4d54 100755 --- a/Tools/px_generate_uorb_topic_headers.py +++ b/Tools/px_generate_uorb_topic_headers.py @@ -90,6 +90,11 @@ def copy_changed(inputdir, outputdir, prefix=''): Copies files from inputdir to outputdir if they don't exist in ouputdir or if their content changed """ + + # Make sure output directory exists: + if not os.path.isdir(outputdir): + os.makedirs(outputdir) + for f in os.listdir(inputdir): fni = os.path.join(inputdir, f) if os.path.isfile(fni): |