summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDaniel Friesel <daniel.friesel@uos.de>2020-09-10 11:45:31 +0200
committerDaniel Friesel <daniel.friesel@uos.de>2020-09-10 11:45:31 +0200
commit8cd97799880032fee3b55e473a8c718479420ba7 (patch)
treebe3340bafd5f3400332f29f2c7099fc3bcfc7720
parentc99e584b769011ec9897246586f74df01bd2f4f4 (diff)
explore-kconfig --neighbourhood: add directory support
-rwxr-xr-xbin/explore-kconfig.py7
1 files changed, 5 insertions, 2 deletions
diff --git a/bin/explore-kconfig.py b/bin/explore-kconfig.py
index 596faff..8887ef1 100755
--- a/bin/explore-kconfig.py
+++ b/bin/explore-kconfig.py
@@ -64,14 +64,17 @@ def main():
if args.random:
for i in range(args.random):
- logging.info(f"Running experiment {i+1} of {args.random}")
+ logging.info(f"Running randconfig {i+1} of {args.random}")
kconf.run_randconfig()
if args.neighbourhood:
if os.path.isfile(args.neighbourhood):
kconf.run_exploration_from_file(args.neighbourhood)
elif os.path.isdir(args.neighbourhood):
- pass
+ for filename in os.listdir(args.neighbourhood):
+ config_filename = f"{args.neighbourhood}/{filename}"
+ logging.info(f"Exploring neighbourhood of {config_filename}")
+ kconf.run_exploration_from_file(config_filename)
else:
print(
f"--neighbourhod: Error: {args.neighbourhood} must be a file or directory, but is neither",