Skip to content

Commit

Permalink
Emit a warning & --no-deps suggestion
Browse files Browse the repository at this point in the history
As per
#176 (comment),
#176 (comment),
and
#176 (comment),
we suggest passing `--no-deps` when `make` complains `Argument list too
long` and `No rule to make target '.*.glob'`.
  • Loading branch information
JasonGross committed Oct 27, 2023
1 parent 46428aa commit f2334e2
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions coq_tools/import_util.py
Original file line number Diff line number Diff line change
Expand Up @@ -485,6 +485,9 @@ def make_globs(logical_names, **kwargs):
make_one_glob_file(v_name, **kwargs)
else:
(stdout_make, stderr_make) = run_coq_makefile_and_make(tuple(sorted(filenames_v + extra_filenames_v)), filenames_glob, **kwargs)
stdouterr_make = stdout_make + stderr_make
if 'Argument list too long' in stdouterr_make and re.search(r"No rule to make target '.*\.glob'", stdouterr_make):
kwargs['log']("WARNING: Making globs may not have succeeded, consider passing " + kwargs['cli_mapping']['use_coq_makefile_for_deps'][False][0])

def get_glob_file_for(filename, update_globs=False, **kwargs):
kwargs = fill_kwargs(kwargs)
Expand Down

0 comments on commit f2334e2

Please sign in to comment.