[SOLVED] What does $$FOO do in bash (in a deb package built with epm)?

What does $$FOO do in bash (in a deb package built with epm)?

On the command line, I get this:

$ FOO=foo
$ echo $FOO
foo
$ echo $$FOO
11971FOO

Here, $$ resolves to the PID of the shell as expected and "FOO" is printed verbatim.

Now, trying to understand and debug some scripts, I find the following:

#!/bin/bash
FILE1=/path/to/file/1
FILE2=/path/to/file/2
echo $$FILE1 >> $$FILE2

The script in question originates from a postinstall script of a Debian package. Is this supposed to undergo pre-processing before it can run?

Update: The script is part of a package built with epm and read via the following directive:

%postinstall <script.sh

In the resulting deb package, the postinst script reads:

#!/bin/bash
FILE1=/path/to/file/1
FILE2=/path/to/file/2
echo $FILE1 >> $FILE2

Thus, the processing is done by either epm or dpkg.

Solution

This is apparently a feature of the EPM packaging tool. Quoting the documentation:

Note that all commands specified in the list file will use the variable expansion provided by EPM, so be sure to quote any dollar sign ($) characters in your commands. For example, "$foo" is replaced by the value of "foo", but "$$foo" becomes "$foo".