You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When the shell used for `sh` is `dash`, which is common on Debian and
its derivatives, the output of the Makefile is incorrect. This patch
resolves the issue by using `bash` as the shell when it's available.
Additionally, I refactored the `push` target to reuse the code that
executes the push command for a specific directory.
Lastly, the default action when you run `make` without any arguments
is now to build all the extensions.
Signed-off-by: Marco Nenciarini <[email protected]>
Signed-off-by: Niccolò Fei <[email protected]>
Co-authored-by: Niccolò Fei <[email protected]>
0 commit comments