widelands-dev team mailing list archive

[GunChleoc <fios@xxxxxxxxxxxxxxxxxxx>]

I replaced 'ls | grep' with '-f' and optimized a bit.

pushd is still an unknown command. If I try this:

    #!/bin/bash

    pushd /etc

I get:

    merge_and_push_translations.sh: 3: merge_and_push_translations.sh: pushd: not found
-- 
https://code.launchpad.net/~widelands-dev/widelands/bug-1219914/+merge/242772
Your team Widelands Developers is subscribed to branch lp:~widelands-dev/widelands/bug-1219914.