Bug#547748: jocaml: bashism in /bin/sh script

[Raphael Geissert <atomo64@gmail.com>]

Package: jocaml
Severity: important
Version: 3.11.1-1
User: debian-release@lists.debian.org
Usertags: goal-dash

Hello maintainer,

While performing an archive wide checkbashisms (from the 'devscripts' package)
check I've found your package containing a /bin/sh script making use
of a bashism.

checkbashisms' output:
> possible bashism in ./usr/bin/jocamlmktop line 7 (alternative test command
> ([[ foo ]] should be [ foo ])):
> if [[ $? -eq 0 ]] ; then
> possible bashism in ./usr/bin/jocamlmktop line 9 (alternative test command
> ([[ foo ]] should be [ foo ])):
>   if [[ "$TOP" == "" ]] ; then
> possible bashism in ./usr/bin/jocamlmktop line 9 (should be 'b = a'):
>   if [[ "$TOP" == "" ]] ; then


Not using bash (or a Debian Policy conformant shell interpreter which doesn't
provide such an extra feature) as /bin/sh is likely to lead to errors or
unexpected behaviours. Please be aware that dash is now the default /bin/sh.

Hints about how to fix bashisms can be found at:
https://wiki.ubuntu.com/DashAsBinSh

If you still don't know how to fix the bashisms don't hesitate to reply to
this email, or tag the bug as 'help'.

Thank you,
Raphael Geissert