Merge branch 'fix/andre/rm-unused-bin-scripts' into 'master'
[dev] remove obsolete scripts See merge request frama-c/frama-c!4722
Showing
- bin/build-src-distrib.sh 0 additions, 837 deletionsbin/build-src-distrib.sh
- bin/frama-c-build-scripts.sh 0 additions, 194 deletionsbin/frama-c-build-scripts.sh
- bin/indent.sh 0 additions, 57 deletionsbin/indent.sh
- bin/merge-master.sh 0 additions, 40 deletionsbin/merge-master.sh
- bin/rebuild.sh 0 additions, 24 deletionsbin/rebuild.sh
- bin/sed_get_binutils_version 0 additions, 1 deletionbin/sed_get_binutils_version
- bin/sed_get_make_major 0 additions, 1 deletionbin/sed_get_make_major
- bin/sed_get_make_minor 0 additions, 1 deletionbin/sed_get_make_minor
- bin/shift_oracles.sh 0 additions, 177 deletionsbin/shift_oracles.sh
Loading
Please register or sign in to comment