1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
#!/bin/bash
#this script should be in $PREFIX/bin
MONO_EXEC="exec -a monodevelop mono"
EXE_PATH="${0%%/bin/monodevelop}/lib/monodevelop/bin/MonoDevelop.exe"
_MD_REDIRECT_LOG="${MD_REDIRECT_LOG:-${XDG_CONFIG_HOME:-$HOME/.config}/MonoDevelop/log}"
_MONO_OPTIONS=$MONO_OPTIONS
#############################
## BEGIN MOZILLA DETECTION ##
#############################
#(NOTE: any changes to this block should be kept in sync with the one in configure.in)
MOZFILE="libgtkembedmoz.so"
find_libgtkembedmoz ()
{
MOZDIR=$MOZILLA_FIVE_HOME
if test -e "$MOZDIR/$MOZFILE"; then echo $MOZDIR; return; fi
ALLMOZDIRS=$(grep -h GRE_PATH= /etc/gre.d/*.conf 2>/dev/null | cut -d '"' -f 2 -d = )
if [ -n "$ALLMOZDIRS" ] ; then
for MOZDIR in $ALLMOZDIRS ; do
if test -e "$MOZDIR/$MOZFILE"; then echo $MOZDIR; return; fi
done
fi
mozilla_script=$(which mozilla 2> /dev/null)
firefox_script=$(which firefox 2> /dev/null)
if [ -z $mozilla_script ] && [ -z $firefox_script ]; then return; fi
for runtime_script in "$firefox_script $mozilla_script"; do
MOZDIR=$(grep "MOZ_DIST_LIB=" $runtime_script 2> /dev/null | cut -d '"' -f 2 | cut -d '=' -f 2)
if test -e "$MOZDIR/$MOZFILE"; then echo $MOZDIR; return; fi
MOZDIR=$(grep "MOZILLA_FIVE_HOME=" $runtime_script 2> /dev/null | cut -d '"' -f 2 | cut -d '=' -f 2)
if test -e "$MOZDIR/$MOZFILE"; then echo $MOZDIR; return; fi
MOZDIR=$(grep "MOZILLA_LIBDIR=" $runtime_script 2> /dev/null | cut -d '"' -f 2 | cut -d '=' -f 2)
if test -e "$MOZDIR/$MOZFILE"; then echo $MOZDIR; return; fi
MOZDIR=$(grep "moz_libdir=" $runtime_script 2> /dev/null | cut -d '"' -f 2 | cut -d '=' -f 2)
if test -e "$MOZDIR/$MOZFILE"; then echo $MOZDIR; return; fi
done
}
if test -e "/$MOZFILE"; then
MOZILLA_HOME=""
else
MOZILLA_HOME=`find_libgtkembedmoz`
if test ! -e "$MOZILLA_HOME/$MOZFILE"; then
MOZILLA_HOME=
echo "WARNING: Cannot find Mozilla directory containing $MOZFILE. Some Addins may not be able to function. Please set MOZILLA_FIVE_HOME to your Mozilla directory."
fi
fi
if [ -n $LD_LIBRARY_PATH ]; then
export LD_LIBRARY_PATH="$MOZILLA_HOME:$LD_LIBRARY_PATH"
else
export LD_LIBRARY_PATH="$MOZILLA_HOME"
fi
export MOZILLA_FIVE_HOME="$MOZILLA_HOME"
###########################
## END MOZILLA DETECTION ##
###########################
if [ -n "$_MD_REDIRECT_LOG" ]; then
mkdir -p `dirname "$_MD_REDIRECT_LOG"`
$MONO_EXEC $_MONO_OPTIONS "$EXE_PATH" $* 2>&1 | tee "$_MD_REDIRECT_LOG"
else
$MONO_EXEC $_MONO_OPTIONS "$EXE_PATH" $*
fi
|