Make the destination folders
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
1da60b3b28
commit
60ba43378a
|
@ -1,6 +1,7 @@
|
||||||
require "json"
|
require "json"
|
||||||
require "set"
|
require "set"
|
||||||
require "optparse"
|
require "optparse"
|
||||||
|
require "fileutils"
|
||||||
|
|
||||||
# For target_dir, use absolute paths because when invoking Agda, we'll be
|
# For target_dir, use absolute paths because when invoking Agda, we'll be
|
||||||
# using chdir.
|
# using chdir.
|
||||||
|
@ -56,6 +57,8 @@ files_for_paths.each do |path, files|
|
||||||
Dir.chdir(original_wd)
|
Dir.chdir(original_wd)
|
||||||
Dir.chdir(File.join(root_path, path))
|
Dir.chdir(File.join(root_path, path))
|
||||||
html_dir = File.join [target_dir, path, "html"]
|
html_dir = File.join [target_dir, path, "html"]
|
||||||
|
FileUtils.mkdir_p html_dir
|
||||||
|
|
||||||
files.each do |file|
|
files.each do |file|
|
||||||
command = "#{ARGV[0]} --local-interfaces #{file} --html --html-dir=#{html_dir}"
|
command = "#{ARGV[0]} --local-interfaces #{file} --html --html-dir=#{html_dir}"
|
||||||
puts command
|
puts command
|
||||||
|
|
Loading…
Reference in New Issue
Block a user