From 292cf009e66e96107f5e2eccb24f04c0ac9a6481 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 18 Aug 2024 12:29:35 -1000 Subject: [PATCH] Remove --local-interfaces as it is no longer needed Signed-off-by: Danila Fedorin --- build-agda-html.rb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build-agda-html.rb b/build-agda-html.rb index ecb86d5..b218bde 100644 --- a/build-agda-html.rb +++ b/build-agda-html.rb @@ -60,7 +60,7 @@ files_for_paths.each do |path, files| FileUtils.mkdir_p html_dir files.each do |file| - command = "#{ARGV[0]} --local-interfaces #{file} --html --html-dir=#{html_dir}" + command = "#{ARGV[0]} #{file} --html --html-dir=#{html_dir}" puts command puts `#{command}`