Skip to content
Snippets Groups Projects
Commit 86bad3e4 authored by Jens Bendisposto's avatar Jens Bendisposto
Browse files

remove binaries from project

parent e0598499
No related branches found
No related tags found
No related merge requests found
Showing
with 0 additions and 66 deletions
Revision: 9938
January 17 2012 - 2002
\ No newline at end of file
File deleted
File deleted
File deleted
File deleted
#!/bin/bash
PROBCOMMAND=probcli
INTERRUPT_COMMAND=send_user_interrupt
# Shell wrapper for PROBCOMMAND
echo "Running ProB Command-line Interface"
echo "$PROBCOMMAND" "$@"
# dirname
dirname=`dirname "$0"`
ulimit -d unlimited
chmod a+x "$dirname/$PROBCOMMAND"
chmod a+x "$dirname/$INTERRUPT_COMMAND"
exec "$dirname/$PROBCOMMAND" "$@"
File deleted
Revision: 9938
January 17 2012 - 1948
\ No newline at end of file
File deleted
File deleted
File deleted
File deleted
#!/bin/bash
PROBCOMMAND=probcli
INTERRUPT_COMMAND=send_user_interrupt
# Shell wrapper for PROBCOMMAND
echo "Running ProB Command-line Interface"
echo "$PROBCOMMAND" "$@"
# dirname
dirname=`dirname "$0"`
ulimit -d unlimited
chmod a+x "$dirname/$PROBCOMMAND"
chmod a+x "$dirname/$INTERRUPT_COMMAND"
exec "$dirname/$PROBCOMMAND" "$@"
File deleted
Revision: 9938
January 17 2012 - 2002
\ No newline at end of file
File deleted
File deleted
File deleted
File deleted
#!/bin/bash
PROBCOMMAND=probcli
INTERRUPT_COMMAND=send_user_interrupt
# Shell wrapper for PROBCOMMAND
echo "Running ProB Command-line Interface"
echo "$PROBCOMMAND" "$@"
# dirname
dirname=`dirname "$0"`
ulimit -d unlimited
chmod a+x "$dirname/$PROBCOMMAND"
chmod a+x "$dirname/$INTERRUPT_COMMAND"
exec "$dirname/$PROBCOMMAND" "$@"
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment