Salutations, Nal,

Depuis quelques années on peut facilement mettre des emojis un peu partout.

Certains se sont dit qu’on pouvait les utiliser en premier caractère des messages de commit Git, ce qui offre divers avantages et inconvénients qu’on va détailler un peu plus loin. L’idée de base est que l’emoji offre un « résumé » très lisible de l’intention du commit, sans avoir à lire le message pour avoir une idée générale de ce qui va se passer dans (…)

J'utilise Gitlab de temps à autre, principalement pour embêter les devs en leur faisant des tickets. En général, une partie de mon temps de rédaction se passe à pester contre ces fichus emojis qui essaient de s'inviter chaque fois que je fais deux points. Je fais beaucoup de liste, dans mes tickets, et ça démarre toujours par cette typographie terrible : deux points. En fait, j'aime bien les deux points pour leur usage de base, qui n'est pas de faire (…)

Le saviez-vous ?

On peut utiliser des emojis en SQL, et pas seulement pour les manipuler : les emojis peuvent servir d'identifieurs !

Avec PostgreSQL, peut donc faire des choses comme :

CREATE TABLE 👤(
    🔑 INTEGER PRIMARY KEY,
    🗣 varchar(64), -- name
    🗓 DATE -- date of registration
);

Voire carrément :

CREATE TYPE ⭐ AS ENUM ('🤢', '☹', '😐', '🙂', '😍');

-- [...]

-- select

Avec l'installation de Ubuntu 18.10 Cosmic, dans Audacity, le raccourci ctrl+shift+e qui me sert à exporter la sélection en mp3 ne fonctionnait plus.

Une grosse perte pour moi qui découpe mes cours de darija en plein de morceaux pour faire des fiches d'apprentissage pour Anki.

Il se trouve que dans Ubuntu 18.10, par défaut, ce raccourci sert désormais à insérer un emoji.

Je suis allé dans système, puis clavier, puis raccourcis pour modifier ce raccourci et je ne l'ai (…)