diff --git a/Manual.md b/Manual.md index 28213191ded..816941e03ab 100644 --- a/Manual.md +++ b/Manual.md @@ -455,6 +455,10 @@ By default set to `make`. `${build_style}` is set to `configure`, `gnu-configure` or `gnu-makefile` build methods. Unset by default. +- `make_check_args` The arguments to be passed in to `${make_cmd}` at the check phase if +`${build_style}` is set to `configure`, `gnu-configure` or `gnu-makefile` +build methods. Unset by default. + - `make_install_args` The arguments to be passed in to `${make_cmd}` at the `install-destdir` phase if `${build_style}` is set to `configure`, `gnu-configure` or `gnu-makefile` build methods. By default set to @@ -464,6 +468,10 @@ phase if `${build_style}` is set to `configure`, `gnu-configure` or `${build_style}` is set to `configure`, `gnu-configure` or `gnu-makefile` build methods. Unset by default (`all` target). +- `make_check_target` The target to be passed in to `${make_cmd}` at the check phase if +`${build_style}` is set to `configure`, `gnu-configure` or `gnu-makefile` +build methods. By default set to `check`. + - `make_install_target` The target to be passed in to `${make_cmd}` at the `install-destdir` phase if `${build_style}` is set to `configure`, `gnu-configure` or `gnu-makefile` build methods. By default set to `install`.