diff options
| author | Stephane Glondu <steph@glondu.net> | 2021-11-23 10:00:21 +0100 |
|---|---|---|
| committer | Stéphane Glondu <Stéphane Glondu glondu@debian.org> | 2021-11-23 10:14:18 +0100 |
| commit | f106d3896fb2ec3b0b3c7e091dd243e6d8b0ae9d (patch) | |
| tree | d8daccae19f5eda4341ed058d272211acf22e345 | |
| parent | 6482b2011277501350b51edc9b78f85b6be61df1 (diff) | |
Use /bin/bash for building doc
| -rwxr-xr-x | debian/rules | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index 00dc711..32f815d 100755 --- a/debian/rules +++ b/debian/rules @@ -11,7 +11,7 @@ override_dh_auto_build-arch: dune build -p visitors,visitors.runtime,visitors.ppx @install override_dh_auto_build-indep: - cd doc && $(MAKE) + cd doc && $(MAKE) SHELL=/bin/bash override_dh_auto_install: # do nothing |