Skip to content

Instantly share code, notes, and snippets.

View cpitclaudel's full-sized avatar

Clément Pit-Claudel cpitclaudel

View GitHub Profile
@zeux
zeux / vcachetester.cpp
Created August 1, 2017 05:23
Source code for "Optimal grid rendering is not optimal" article.
#include <d3d11.h>
#include <d3dcompiler.h>
#include <stdio.h>
#include <assert.h>
#include <cassert>
#include <cmath>
#include <vector>
#pragma comment (lib, "d3d11.lib")
@plaidfinch
plaidfinch / Ding.el
Last active August 5, 2016 06:56
Configure flycheck to make a "ding!" sound after it completes checking, only in certain modes
;; Noisy Flycheck (for slow syntax checkers, program verifiers, &c.)
(defvar flycheck-ding t) ;; Enable sounds?
(defvar flycheck-ding-path "~/.emacs.d/private/Ding.mp3") ;; Where's the "ding!" sound to make?
(defvar flycheck-buzz-path "~/.emacs.d/private/Basso.aiff") ;; Where's the "bzz!" sound to make?
(defvar flycheck-noisy-modes-list '(dafny-mode)) ;; Which modes should we make sounds in?
;; Below what number of seconds checking time should we be silent?
(defvar flycheck-ding-delay-threshold 2)
(defvar flycheck-buzz-delay-threshold 1)
@ssp
ssp / git-extract-file.markdown
Created January 23, 2012 13:21
Extract a single file from a git repository

How to extract a single file with its history from a git repository

These steps show two less common interactions with git to extract a single file which is inside a subfolder from a git repository. These steps essentially reduce the repository to just the desired files and should performed on a copy of the original repository (1.).

First the repository is reduced to just the subfolder containing the files in question using git filter-branch --subdirectory-filter (2.) which is a useful step by itself if just a subfolder needs to be extracted. This step moves the desired files to the top level of the repository.

Finally all remaining files are listed using git ls, the files to keep are removed from that using grep -v and the resulting list is passed to git rm which is invoked by git filter-branch --index-filter (3.). A bit convoluted but it does the trick.

1. copy the repository to extract the file from and go to the desired branch