MiguelMJ

#!/usr/bin/bash
# original source: https://engineering.giphy.com/how-to-make-gifs-with-ffmpeg/

in="$1"
out="$2"
start="$3"
length="$4"

ffmpeg -ss $start -t $length -i "$in" -filter_complex "[0:v] fps=12,scale=480:-1,split [a][b];[a] palettegen [p];[b][p] paletteuse" "$out"

MiguelMJ

#!/usr/bin/bash
# Usage: ./mindoxifile.sh Doxyfile
# The Doxyfile will be minimized and will only contain the non-default values
set -e

defaultdoxy=".defdoxy"
doxygen -s -g $defaultdoxy > /dev/null
grep -v "^#" $defaultdoxy | sed ':a;N;$!ba;s/\\\n/\\n/g' | sort > "$defaultdoxy.sorted"
mv "$defaultdoxy.sorted" "$defaultdoxy"

MiguelMJ

#!/usr/bin/bash
#
# Create a bootable USB from a local or remote ISO image
#
# Based on the tutorial from https://www.pragmaticlinux.com/2021/03/create-a-bootable-usb-drive-from-a-linux-iso-image/
#
# IMPORTANT: This script does not sanitize any input, make sure to introduce it well or modify it to make it safer 

# Select external disk
echo "List of detected disks"

MiguelMJ

# Source this file from .bashrc
# or copy the code inside it
ws(){
    print_help(){
        echo "usage: ws [-s] [options]"
        echo ""
        echo "options:"
        echo "  -h          print this help message"
        echo "  -s          change workspace or apply certain operations to workspaces"
        echo "  -a          add current directory to active workspace"