From b5078fd65f0eaf6c9f1a67094afe37d794ee8913 Mon Sep 17 00:00:00 2001
From: Zuzana Baranova <xbaranov@fi.muni.cz>
Date: Wed, 12 Dec 2018 20:02:28 +0000
Subject: [PATCH] tools: Allow multiple files with -o in divcc if they are
libraries.
---
tools/divcc.cpp | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/tools/divcc.cpp b/tools/divcc.cpp
index 13955d921..beef9d6c5 100644
--- a/tools/divcc.cpp
+++ b/tools/divcc.cpp
@@ -1,4 +1,5 @@
#include <divine/cc/cc1.hpp>
+#include <divine/cc/filetype.hpp>
#include <divine/cc/options.hpp>
#include <divine/rt/dios-cc.hpp>
#include <divine/rt/runtime.hpp>
@@ -287,7 +288,11 @@ int main( int argc, char **argv )
, "-isystem", joinPath( includeDir, "libunwind/include" )
, "-isystem", includeDir } );
- if ( po.files.size() > 1 && po.outputFile != ""
+ // count files, i.e. not libraries
+ auto num_files = std::count_if( po.files.begin(), po.files.end(),
+ []( cc::FileEntry f ){ return f.is< cc::File >(); } );
+
+ if ( num_files > 1 && po.outputFile != ""
&& ( po.preprocessOnly || po.toObjectOnly ) )
{
std::cerr << "Cannot specify -o with multiple files" << std::endl;
--
GitLab