[dev] remove local-export.sh and update scripts
Showing
- bin/dune 0 additions, 1 deletionbin/dune
- bin/frama-c-gui.byte 0 additions, 27 deletionsbin/frama-c-gui.byte
- bin/frama-c.byte 0 additions, 27 deletionsbin/frama-c.byte
- bin/frama-c.top 0 additions, 27 deletionsbin/frama-c.top
- bin/local_export.sh 0 additions, 30 deletionsbin/local_export.sh
- dev/frama-c-callgrind.sh 2 additions, 8 deletionsdev/frama-c-callgrind.sh
bin/frama-c-gui.byte
deleted
100755 → 0
bin/frama-c.byte
deleted
100755 → 0
bin/frama-c.top
deleted
100755 → 0
bin/local_export.sh
deleted
100644 → 0
Please register or sign in to comment